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