Metamath Proof Explorer

Theorem trcleq2lem

Description: Equality implies bijection. (Contributed by RP, 5-May-2020)

Ref Expression
Assertion trcleq2lem 
|- ( A = B -> ( ( R C_ A /\ ( A o. A ) C_ A ) <-> ( R C_ B /\ ( B o. B ) C_ B ) ) )

Proof

Step Hyp Ref Expression
1 sseq2 
 |-  ( A = B -> ( R C_ A <-> R C_ B ) )
2 id 
 |-  ( A = B -> A = B )
3 2 2 coeq12d 
 |-  ( A = B -> ( A o. A ) = ( B o. B ) )
4 3 2 sseq12d 
 |-  ( A = B -> ( ( A o. A ) C_ A <-> ( B o. B ) C_ B ) )
5 1 4 anbi12d 
 |-  ( A = B -> ( ( R C_ A /\ ( A o. A ) C_ A ) <-> ( R C_ B /\ ( B o. B ) C_ B ) ) )