Metamath Proof Explorer

Theorem trujust

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

Ref Expression
Assertion trujust 
|- ( ( A. x x = x -> A. x x = x ) <-> ( A. y y = y -> A. y y = y ) )

Proof

Step Hyp Ref Expression
1 monothetic 
 |-  ( ( A. x x = x -> A. x x = x ) <-> ( A. y y = y -> A. y y = y ) )