Theorem gdlopcfvlem

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

	Ref	Expression
Hypotheses	gdlopcfvlem.1	⊢ 𝐴 ∈ On
	gdlopcfvlem.2	⊢ 𝐵 ∈ On
	gdlopcfvlem.3	⊢ 𝐴 ∈ 𝐵
Assertion	gdlopcfvlem	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → if ( 𝐶 = 𝐴 , 𝐷 , 𝐸 ) = 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		gdlopcfvlem.1	⊢ 𝐴 ∈ On
2		gdlopcfvlem.2	⊢ 𝐵 ∈ On
3		gdlopcfvlem.3	⊢ 𝐴 ∈ 𝐵
4		onelpss	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵 ) ) )
5	1 2 4	mp2an	⊢ ( 𝐴 ∈ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )
6	3 5	mpbi	⊢ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵 )
7	6	simpri	⊢ 𝐴 ≠ 𝐵
8		neeq2	⊢ ( 𝐵 = 𝐶 → ( 𝐴 ≠ 𝐵 ↔ 𝐴 ≠ 𝐶 ) )
9	7 8	mpbii	⊢ ( 𝐵 = 𝐶 → 𝐴 ≠ 𝐶 )
10		nesym	⊢ ( 𝐴 ≠ 𝐶 ↔ ¬ 𝐶 = 𝐴 )
11	9 10	sylib	⊢ ( 𝐵 = 𝐶 → ¬ 𝐶 = 𝐴 )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ¬ 𝐶 = 𝐴 )
13	12	iffalsed	⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → if ( 𝐶 = 𝐴 , 𝐷 , 𝐸 ) = 𝐸 )