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 ∈ B x = y ∨ C ∩ D = ∅ ↔ ∀ x ∈ A ∀ z ∀ y ∈ B z ∈ 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 = ∅ ↔ ∃ z z ∈ C ∩ D
4 elin ⊢ z ∈ C ∩ D ↔ z ∈ C ∧ z ∈ D
5 4 exbii ⊢ ∃ z z ∈ C ∩ D ↔ ∃ z z ∈ C ∧ z ∈ D
6 3 5 bitri ⊢ ¬ C ∩ D = ∅ ↔ ∃ z z ∈ C ∧ z ∈ D
7 6 imbi1i ⊢ ¬ C ∩ D = ∅ → x = y ↔ ∃ z z ∈ C ∧ z ∈ D → x = y
8 19.23v ⊢ ∀ z z ∈ C ∧ z ∈ D → x = y ↔ ∃ z z ∈ C ∧ z ∈ D → x = y
9 7 8 bitr4i ⊢ ¬ C ∩ D = ∅ → x = y ↔ ∀ z z ∈ C ∧ z ∈ D → x = y
10 1 2 9 3bitri ⊢ x = y ∨ C ∩ D = ∅ ↔ ∀ z z ∈ C ∧ z ∈ D → x = y
11 10 ralbii ⊢ ∀ y ∈ B x = y ∨ C ∩ D = ∅ ↔ ∀ y ∈ B ∀ z z ∈ C ∧ z ∈ D → x = y
12 ralcom4 ⊢ ∀ y ∈ B ∀ z z ∈ C ∧ z ∈ D → x = y ↔ ∀ z ∀ y ∈ B z ∈ C ∧ z ∈ D → x = y
13 11 12 bitri ⊢ ∀ y ∈ B x = y ∨ C ∩ D = ∅ ↔ ∀ z ∀ y ∈ B z ∈ C ∧ z ∈ D → x = y
14 13 ralbii ⊢ ∀ x ∈ A ∀ y ∈ B x = y ∨ C ∩ D = ∅ ↔ ∀ x ∈ A ∀ z ∀ y ∈ B z ∈ C ∧ z ∈ D → x = y