This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eupth2lem1

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

Ref Expression
Assertion eupth2lem1 ⊢ U ∈ V → U ∈ if A = B ∅ A B ↔ A ≠ B ∧ U = A ∨ U = B

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ ∅ = if A = B ∅ A B → U ∈ ∅ ↔ U ∈ if A = B ∅ A B
2 1 bibi1d ⊢ ∅ = if A = B ∅ A B → U ∈ ∅ ↔ A ≠ B ∧ U = A ∨ U = B ↔ U ∈ if A = B ∅ A B ↔ A ≠ B ∧ U = A ∨ U = B
3 eleq2 ⊢ A B = if A = B ∅ A B → U ∈ A B ↔ U ∈ if A = B ∅ A B
4 3 bibi1d ⊢ A B = if A = B ∅ A B → U ∈ A B ↔ A ≠ B ∧ U = A ∨ U = B ↔ U ∈ if A = B ∅ A B ↔ A ≠ B ∧ U = A ∨ U = B
5 noel ⊢ ¬ U ∈ ∅
6 5 a1i ⊢ U ∈ V ∧ A = B → ¬ U ∈ ∅
7 simpl ⊢ A ≠ B ∧ U = A ∨ U = B → A ≠ B
8 7 neneqd ⊢ A ≠ B ∧ U = A ∨ U = B → ¬ A = B
9 simpr ⊢ U ∈ V ∧ A = B → A = B
10 8 9 nsyl3 ⊢ U ∈ V ∧ A = B → ¬ A ≠ B ∧ U = A ∨ U = B
11 6 10 2falsed ⊢ U ∈ V ∧ A = B → U ∈ ∅ ↔ A ≠ B ∧ U = A ∨ U = B
12 elprg ⊢ U ∈ V → U ∈ A B ↔ U = A ∨ U = B
13 df-ne ⊢ A ≠ B ↔ ¬ A = B
14 ibar ⊢ A ≠ B → U = A ∨ U = B ↔ A ≠ B ∧ U = A ∨ U = B
15 13 14 sylbir ⊢ ¬ A = B → U = A ∨ U = B ↔ A ≠ B ∧ U = A ∨ U = B
16 12 15 sylan9bb ⊢ U ∈ V ∧ ¬ A = B → U ∈ A B ↔ A ≠ B ∧ U = A ∨ U = B
17 2 4 11 16 ifbothda ⊢ U ∈ V → U ∈ if A = B ∅ A B ↔ A ≠ B ∧ U = A ∨ U = B