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

Metamath Proof Explorer

Theorem ineleq

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

Ref Expression
Assertion ineleq ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶 ∩ 𝐷 ) = ∅ ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) → 𝑥 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 orcom ⊢ ( ( 𝑥 = 𝑦 ∨ ( 𝐶 ∩ 𝐷 ) = ∅ ) ↔ ( ( 𝐶 ∩ 𝐷 ) = ∅ ∨ 𝑥 = 𝑦 ) )
2 df-or ⊢ ( ( ( 𝐶 ∩ 𝐷 ) = ∅ ∨ 𝑥 = 𝑦 ) ↔ ( ¬ ( 𝐶 ∩ 𝐷 ) = ∅ → 𝑥 = 𝑦 ) )
3 neq0 ⊢ ( ¬ ( 𝐶 ∩ 𝐷 ) = ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝐶 ∩ 𝐷 ) )
4 elin ⊢ ( 𝑧 ∈ ( 𝐶 ∩ 𝐷 ) ↔ ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) )
5 4 exbii ⊢ ( ∃ 𝑧 𝑧 ∈ ( 𝐶 ∩ 𝐷 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) )
6 3 5 bitri ⊢ ( ¬ ( 𝐶 ∩ 𝐷 ) = ∅ ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) )
7 6 imbi1i ⊢ ( ( ¬ ( 𝐶 ∩ 𝐷 ) = ∅ → 𝑥 = 𝑦 ) ↔ ( ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) → 𝑥 = 𝑦 ) )
8 19.23v ⊢ ( ∀ 𝑧 ( ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) → 𝑥 = 𝑦 ) ↔ ( ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) → 𝑥 = 𝑦 ) )
9 7 8 bitr4i ⊢ ( ( ¬ ( 𝐶 ∩ 𝐷 ) = ∅ → 𝑥 = 𝑦 ) ↔ ∀ 𝑧 ( ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) → 𝑥 = 𝑦 ) )
10 1 2 9 3bitri ⊢ ( ( 𝑥 = 𝑦 ∨ ( 𝐶 ∩ 𝐷 ) = ∅ ) ↔ ∀ 𝑧 ( ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) → 𝑥 = 𝑦 ) )
11 10 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶 ∩ 𝐷 ) = ∅ ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) → 𝑥 = 𝑦 ) )
12 ralcom4 ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ( ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑧 ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) → 𝑥 = 𝑦 ) )
13 11 12 bitri ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶 ∩ 𝐷 ) = ∅ ) ↔ ∀ 𝑧 ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) → 𝑥 = 𝑦 ) )
14 13 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶 ∩ 𝐷 ) = ∅ ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 ∈ 𝐶 ∧ 𝑧 ∈ 𝐷 ) → 𝑥 = 𝑦 ) )