Theorem trujust

Soundness justification theorem for [df-tru]. Instance of monothetic. (Contributed by Mario Carneiro, 17-Nov-2013.) (Revised by NM, 11-Jul-2019.)

Conclusion

\( \vdash \forall x \, x = x \rightarrow \forall x \, x = x \leftrightarrow \forall y \, y = y \rightarrow \forall y \, y = y \)

Proof

monothetic