Theorem gdlopcfvlem

Description: Lemma for gdlopcfv2 through gdlopcfv8 . (Contributed by BTernaryTau, 19-Oct-2026)

	Ref	Expression
Hypotheses	gdlopcfvlem.1	|- A e. On
	gdlopcfvlem.2	|- B e. On
	gdlopcfvlem.3	|- A e. B
Assertion	gdlopcfvlem	|- ( ( ph /\ B = C ) -> if ( C = A , D , E ) = E )

Proof

Step	Hyp	Ref	Expression
1		gdlopcfvlem.1	|- A e. On
2		gdlopcfvlem.2	|- B e. On
3		gdlopcfvlem.3	|- A e. B
4		onelpss	|- ( ( A e. On /\ B e. On ) -> ( A e. B <-> ( A C_ B /\ A =/= B ) ) )
5	1 2 4	mp2an	|- ( A e. B <-> ( A C_ B /\ A =/= B ) )
6	3 5	mpbi	|- ( A C_ B /\ A =/= B )
7	6	simpri	|- A =/= B
8		neeq2	|- ( B = C -> ( A =/= B <-> A =/= C ) )
9	7 8	mpbii	|- ( B = C -> A =/= C )
10		nesym	|- ( A =/= C <-> -. C = A )
11	9 10	sylib	|- ( B = C -> -. C = A )
12	11	adantl	|- ( ( ph /\ B = C ) -> -. C = A )
13	12	iffalsed	|- ( ( ph /\ B = C ) -> if ( C = A , D , E ) = E )