Theorem gdlopcfvlem

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

	Ref	Expression
Hypotheses	gdlopcfvlem.1	$$⊢A\in \mathrm{On}$$
	gdlopcfvlem.2	$$⊢B\in \mathrm{On}$$
	gdlopcfvlem.3	$$⊢A\in B$$
Assertion	gdlopcfvlem	$$⊢\left(\phi \wedge B=C\right)\to if\left(C=A,D,E\right)=E$$

Proof

Step	Hyp	Ref	Expression
1		gdlopcfvlem.1	$$⊢A\in \mathrm{On}$$
2		gdlopcfvlem.2	$$⊢B\in \mathrm{On}$$
3		gdlopcfvlem.3	$$⊢A\in B$$
4		onelpss	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\in B\leftrightarrow \left(A\subseteq B\wedge A\ne B\right)\right)$$
5	1 2 4	mp2an	$$⊢A\in B\leftrightarrow \left(A\subseteq B\wedge A\ne B\right)$$
6	3 5	mpbi	$$⊢\left(A\subseteq B\wedge A\ne B\right)$$
7	6	simpri	$$⊢A\ne B$$
8		neeq2	$$⊢B=C\to \left(A\ne B\leftrightarrow A\ne C\right)$$
9	7 8	mpbii	$$⊢B=C\to A\ne C$$
10		nesym	$$⊢A\ne C\leftrightarrow \neg C=A$$
11	9 10	sylib	$$⊢B=C\to \neg C=A$$
12	11	adantl	$$⊢\left(\phi \wedge B=C\right)\to \neg C=A$$
13	12	iffalsed	$$⊢\left(\phi \wedge B=C\right)\to if\left(C=A,D,E\right)=E$$