Metamath Proof Explorer

Theorem eupth2lem1

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

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

Proof

Step Hyp Ref Expression
1 eleq2 ⊢∅=ifA=B∅AB→U∈∅↔U∈ifA=B∅AB
2 1 bibi1d ⊢∅=ifA=B∅AB→U∈∅↔A≠B∧U=A∨U=B↔U∈ifA=B∅AB↔A≠B∧U=A∨U=B
3 eleq2 ⊢AB=ifA=B∅AB→U∈AB↔U∈ifA=B∅AB
4 3 bibi1d ⊢AB=ifA=B∅AB→U∈AB↔A≠B∧U=A∨U=B↔U∈ifA=B∅AB↔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∈AB↔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∈AB↔A≠B∧U=A∨U=B
17 2 4 11 16 ifbothda ⊢U∈V→U∈ifA=B∅AB↔A≠B∧U=A∨U=B