Theorem eupth2lem1

Description: Lemma for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015)

	Ref	Expression
Assertion	eupth2lem1	⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq2	⊢ ( ∅ = if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) → ( 𝑈 ∈ ∅ ↔ 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ) )
2	1	bibi1d	⊢ ( ∅ = if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) → ( ( 𝑈 ∈ ∅ ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) ) ↔ ( 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) ) ) )
3		eleq2	⊢ ( { 𝐴 , 𝐵 } = if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) → ( 𝑈 ∈ { 𝐴 , 𝐵 } ↔ 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ) )
4	3	bibi1d	⊢ ( { 𝐴 , 𝐵 } = if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) → ( ( 𝑈 ∈ { 𝐴 , 𝐵 } ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) ) ↔ ( 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) ) ) )
5		noel	⊢ ¬ 𝑈 ∈ ∅
6	5	a1i	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → ¬ 𝑈 ∈ ∅ )
7		simpl	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) → 𝐴 ≠ 𝐵 )
8	7	neneqd	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) → ¬ 𝐴 = 𝐵 )
9		simpr	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
10	8 9	nsyl3	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → ¬ ( 𝐴 ≠ 𝐵 ∧ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) )
11	6 10	2falsed	⊢ ( ( 𝑈 ∈ 𝑉 ∧ 𝐴 = 𝐵 ) → ( 𝑈 ∈ ∅ ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) ) )
12		elprg	⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) )
13		df-ne	⊢ ( 𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵 )
14		ibar	⊢ ( 𝐴 ≠ 𝐵 → ( ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) ) )
15	13 14	sylbir	⊢ ( ¬ 𝐴 = 𝐵 → ( ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) ) )
16	12 15	sylan9bb	⊢ ( ( 𝑈 ∈ 𝑉 ∧ ¬ 𝐴 = 𝐵 ) → ( 𝑈 ∈ { 𝐴 , 𝐵 } ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) ) )
17	2 4 11 16	ifbothda	⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝑈 = 𝐴 ∨ 𝑈 = 𝐵 ) ) ) )