Theorem cleq1lem

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

	Ref	Expression
Assertion	cleq1lem	|- ( A = B -> ( ( A C_ C /\ ph ) <-> ( B C_ C /\ ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		sseq1	|- ( A = B -> ( A C_ C <-> B C_ C ) )
2	1	anbi1d	|- ( A = B -> ( ( A C_ C /\ ph ) <-> ( B C_ C /\ ph ) ) )