Metamath Proof Explorer

Theorem trcleq12lem

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

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

Step	Hyp	Ref	Expression
1		cleq1lem	\|- ( R = S -> ( ( R C_ A /\ ( A o. A ) C_ A ) <-> ( S C_ A /\ ( A o. A ) C_ A ) ) )
2		trcleq2lem	\|- ( A = B -> ( ( S C_ A /\ ( A o. A ) C_ A ) <-> ( S C_ B /\ ( B o. B ) C_ B ) ) )
3	1 2	sylan9bb	\|- ( ( R = S /\ A = B ) -> ( ( R C_ A /\ ( A o. A ) C_ A ) <-> ( S C_ B /\ ( B o. B ) C_ B ) ) )

Step

Hyp

Ref

Expression

 |-  ( R = S -> ( ( R C_ A /\ ( A o. A ) C_ A ) <-> ( S C_ A /\ ( A o. A ) C_ A ) ) )

 |-  ( A = B -> ( ( S C_ A /\ ( A o. A ) C_ A ) <-> ( S C_ B /\ ( B o. B ) C_ B ) ) )

1 2

 |-  ( ( R = S /\ A = B ) -> ( ( R C_ A /\ ( A o. A ) C_ A ) <-> ( S C_ B /\ ( B o. B ) C_ B ) ) )