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 ( ∀ 𝑥𝐴𝑦𝐵 ( 𝑥 = 𝑦 ∨ ( 𝐶𝐷 ) = ∅ ) ↔ ∀ 𝑥𝐴𝑧𝑦𝐵 ( ( 𝑧𝐶𝑧𝐷 ) → 𝑥 = 𝑦 ) )