Metamath Proof Explorer

Theorem heeq1

Description: Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020)

Ref Expression
Assertion heeq1 
|- ( R = S -> ( R hereditary A <-> S hereditary A ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  A = A
2 heeq12 
 |-  ( ( R = S /\ A = A ) -> ( R hereditary A <-> S hereditary A ) )
3 1 2 mpan2 
 |-  ( R = S -> ( R hereditary A <-> S hereditary A ) )