Theorem 2reu5 3045

Description: Double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, analogous to 2eu5 2288 and reu3 3027. (Contributed by Alexander van der Vekens, 17-Jun-2017.)

Assertion

Ref	Expression
2reu5	⊢ ((∃!x ∈ A ∃!y ∈ B φ ∧ ∀x ∈ A ∃*y ∈ B φ) ↔ (∃x ∈ A ∃y ∈ B φ ∧ ∃z ∈ A ∃w ∈ B ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))))

Distinct variable groups:   y,w,z,A,x   w,B   x,z,B,y   φ,w,z   x,A   y,B

Allowed substitution hints:   φ(x, y)

Proof of Theorem 2reu5

Step	Hyp	Ref	Expression
1		r19.29r 2756	. . . . . . . 8 ⊢ ((∃x ∈ A ∃y ∈ B φ ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))) → ∃x ∈ A (∃y ∈ B φ ∧ ∀y ∈ B (φ → (x = z ∧ y = w))))
2		r19.29r 2756	. . . . . . . . 9 ⊢ ((∃y ∈ B φ ∧ ∀y ∈ B (φ → (x = z ∧ y = w))) → ∃y ∈ B (φ ∧ (φ → (x = z ∧ y = w))))
3	2	reximi 2722	. . . . . . . 8 ⊢ (∃x ∈ A (∃y ∈ B φ ∧ ∀y ∈ B (φ → (x = z ∧ y = w))) → ∃x ∈ A ∃y ∈ B (φ ∧ (φ → (x = z ∧ y = w))))
4		pm3.35 570	. . . . . . . . . . 11 ⊢ ((φ ∧ (φ → (x = z ∧ y = w))) → (x = z ∧ y = w))
5	4	reximi 2722	. . . . . . . . . 10 ⊢ (∃y ∈ B (φ ∧ (φ → (x = z ∧ y = w))) → ∃y ∈ B (x = z ∧ y = w))
6	5	reximi 2722	. . . . . . . . 9 ⊢ (∃x ∈ A ∃y ∈ B (φ ∧ (φ → (x = z ∧ y = w))) → ∃x ∈ A ∃y ∈ B (x = z ∧ y = w))
7		eleq1 2413	. . . . . . . . . . . . . 14 ⊢ (x = z → (x ∈ A ↔ z ∈ A))
8		eleq1 2413	. . . . . . . . . . . . . 14 ⊢ (y = w → (y ∈ B ↔ w ∈ B))
9	7, 8	bi2anan9 843	. . . . . . . . . . . . 13 ⊢ ((x = z ∧ y = w) → ((x ∈ A ∧ y ∈ B) ↔ (z ∈ A ∧ w ∈ B)))
10	9	biimpac 472	. . . . . . . . . . . 12 ⊢ (((x ∈ A ∧ y ∈ B) ∧ (x = z ∧ y = w)) → (z ∈ A ∧ w ∈ B))
11	10	ancomd 438	. . . . . . . . . . 11 ⊢ (((x ∈ A ∧ y ∈ B) ∧ (x = z ∧ y = w)) → (w ∈ B ∧ z ∈ A))
12	11	ex 423	. . . . . . . . . 10 ⊢ ((x ∈ A ∧ y ∈ B) → ((x = z ∧ y = w) → (w ∈ B ∧ z ∈ A)))
13	12	rexlimivv 2744	. . . . . . . . 9 ⊢ (∃x ∈ A ∃y ∈ B (x = z ∧ y = w) → (w ∈ B ∧ z ∈ A))
14	6, 13	syl 15	. . . . . . . 8 ⊢ (∃x ∈ A ∃y ∈ B (φ ∧ (φ → (x = z ∧ y = w))) → (w ∈ B ∧ z ∈ A))
15	1, 3, 14	3syl 18	. . . . . . 7 ⊢ ((∃x ∈ A ∃y ∈ B φ ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))) → (w ∈ B ∧ z ∈ A))
16	15	ex 423	. . . . . 6 ⊢ (∃x ∈ A ∃y ∈ B φ → (∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)) → (w ∈ B ∧ z ∈ A)))
17	16	pm4.71rd 616	. . . . 5 ⊢ (∃x ∈ A ∃y ∈ B φ → (∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)) ↔ ((w ∈ B ∧ z ∈ A) ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)))))
18		anass 630	. . . . 5 ⊢ (((w ∈ B ∧ z ∈ A) ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))) ↔ (w ∈ B ∧ (z ∈ A ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)))))
19	17, 18	syl6bb 252	. . . 4 ⊢ (∃x ∈ A ∃y ∈ B φ → (∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)) ↔ (w ∈ B ∧ (z ∈ A ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))))))
20	19	2exbidv 1628	. . 3 ⊢ (∃x ∈ A ∃y ∈ B φ → (∃z∃w∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)) ↔ ∃z∃w(w ∈ B ∧ (z ∈ A ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))))))
21	20	pm5.32i 618	. 2 ⊢ ((∃x ∈ A ∃y ∈ B φ ∧ ∃z∃w∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))) ↔ (∃x ∈ A ∃y ∈ B φ ∧ ∃z∃w(w ∈ B ∧ (z ∈ A ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))))))
22		2reu5lem3 3044	. 2 ⊢ ((∃!x ∈ A ∃!y ∈ B φ ∧ ∀x ∈ A ∃*y ∈ B φ) ↔ (∃x ∈ A ∃y ∈ B φ ∧ ∃z∃w∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))))
23		df-rex 2621	. . . 4 ⊢ (∃z ∈ A ∃w ∈ B ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)) ↔ ∃z(z ∈ A ∧ ∃w ∈ B ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))))
24		r19.42v 2766	. . . . . 6 ⊢ (∃w ∈ B (z ∈ A ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))) ↔ (z ∈ A ∧ ∃w ∈ B ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))))
25		df-rex 2621	. . . . . 6 ⊢ (∃w ∈ B (z ∈ A ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))) ↔ ∃w(w ∈ B ∧ (z ∈ A ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)))))
26	24, 25	bitr3i 242	. . . . 5 ⊢ ((z ∈ A ∧ ∃w ∈ B ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))) ↔ ∃w(w ∈ B ∧ (z ∈ A ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)))))
27	26	exbii 1582	. . . 4 ⊢ (∃z(z ∈ A ∧ ∃w ∈ B ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))) ↔ ∃z∃w(w ∈ B ∧ (z ∈ A ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)))))
28	23, 27	bitri 240	. . 3 ⊢ (∃z ∈ A ∃w ∈ B ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)) ↔ ∃z∃w(w ∈ B ∧ (z ∈ A ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)))))
29	28	anbi2i 675	. 2 ⊢ ((∃x ∈ A ∃y ∈ B φ ∧ ∃z ∈ A ∃w ∈ B ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))) ↔ (∃x ∈ A ∃y ∈ B φ ∧ ∃z∃w(w ∈ B ∧ (z ∈ A ∧ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))))))
30	21, 22, 29	3bitr4i 268	1 ⊢ ((∃!x ∈ A ∃!y ∈ B φ ∧ ∀x ∈ A ∃*y ∈ B φ) ↔ (∃x ∈ A ∃y ∈ B φ ∧ ∃z ∈ A ∃w ∈ B ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 176   ∧ wa 358  ∃wex 1541   ∈ wcel 1710  ∀wral 2615  ∃wrex 2616  ∃!wreu 2617  ∃*wrmo 2618

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This proof depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-cleq 2346  df-clel 2349  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623

This theorem is used by: (None)