Theorem cleq2lem

Description: Equality implies bijection. (Contributed by RP, 24-Jul-2020)

	Ref	Expression
Hypothesis	cleq2lem.b	|- ( A = B -> ( ph <-> ps ) )
Assertion	cleq2lem	|- ( A = B -> ( ( R C_ A /\ ph ) <-> ( R C_ B /\ ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		cleq2lem.b	|- ( A = B -> ( ph <-> ps ) )
2		sseq2	|- ( A = B -> ( R C_ A <-> R C_ B ) )
3	2 1	anbi12d	|- ( A = B -> ( ( R C_ A /\ ph ) <-> ( R C_ B /\ ps ) ) )