Metamath Proof Explorer

Theorem ineleq

Description: Equivalence of restricted universal quantifications. (Contributed by Peter Mazsa, 29-May-2018)

Ref Expression
Assertion ineleq ⊢∀x∈A∀y∈Bx=y∨C∩D=∅↔∀x∈A∀z∀y∈Bz∈C∧z∈D→x=y

Proof

Step Hyp Ref Expression
1 orcom ⊢x=y∨C∩D=∅↔C∩D=∅∨x=y
2 df-or ⊢C∩D=∅∨x=y↔¬C∩D=∅→x=y
3 neq0 ⊢¬C∩D=∅↔∃zz∈C∩D
4 elin ⊢z∈C∩D↔z∈C∧z∈D
5 4 exbii ⊢∃zz∈C∩D↔∃zz∈C∧z∈D
6 3 5 bitri ⊢¬C∩D=∅↔∃zz∈C∧z∈D
7 6 imbi1i ⊢¬C∩D=∅→x=y↔∃zz∈C∧z∈D→x=y
8 19.23v ⊢∀zz∈C∧z∈D→x=y↔∃zz∈C∧z∈D→x=y
9 7 8 bitr4i ⊢¬C∩D=∅→x=y↔∀zz∈C∧z∈D→x=y
10 1 2 9 3bitri ⊢x=y∨C∩D=∅↔∀zz∈C∧z∈D→x=y
11 10 ralbii ⊢∀y∈Bx=y∨C∩D=∅↔∀y∈B∀zz∈C∧z∈D→x=y
12 ralcom4 ⊢∀y∈B∀zz∈C∧z∈D→x=y↔∀z∀y∈Bz∈C∧z∈D→x=y
13 11 12 bitri ⊢∀y∈Bx=y∨C∩D=∅↔∀z∀y∈Bz∈C∧z∈D→x=y
14 13 ralbii ⊢∀x∈A∀y∈Bx=y∨C∩D=∅↔∀x∈A∀z∀y∈Bz∈C∧z∈D→x=y