Metamath Proof Explorer

Theorem trcleq2lemRP

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

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

Proof

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