Metamath Proof Explorer

Theorem heeq2

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

Ref Expression
Assertion heeq2 
|- ( A = B -> ( R hereditary A <-> R hereditary B ) )

Proof

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