Theorem 2reu5lem3 3044

Description: Lemma for 2reu5 3045. This lemma is interesting in its own right, showing that existential restriction in the last conjunct (the "at most one" part) is optional; compare rmo2 3132. (Contributed by Alexander van der Vekens, 17-Jun-2017.)

Assertion

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

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

Allowed substitution hints:   φ(x,y)   A(x)   B(y)

Proof of Theorem 2reu5lem3

Step	Hyp	Ref	Expression
1		2reu5lem1 3042	. . 3 ⊢ (∃!x ∈ A ∃!y ∈ B φ ↔ ∃!x∃!y(x ∈ A ∧ y ∈ B ∧ φ))
2		2reu5lem2 3043	. . 3 ⊢ (∀x ∈ A ∃*y ∈ B φ ↔ ∀x∃*y(x ∈ A ∧ y ∈ B ∧ φ))
3	1, 2	anbi12i 678	. 2 ⊢ ((∃!x ∈ A ∃!y ∈ B φ ∧ ∀x ∈ A ∃*y ∈ B φ) ↔ (∃!x∃!y(x ∈ A ∧ y ∈ B ∧ φ) ∧ ∀x∃*y(x ∈ A ∧ y ∈ B ∧ φ)))
4		2eu5 2288	. 2 ⊢ ((∃!x∃!y(x ∈ A ∧ y ∈ B ∧ φ) ∧ ∀x∃*y(x ∈ A ∧ y ∈ B ∧ φ)) ↔ (∃x∃y(x ∈ A ∧ y ∈ B ∧ φ) ∧ ∃z∃w∀x∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w))))
5		3anass 938	. . . . . . 7 ⊢ ((x ∈ A ∧ y ∈ B ∧ φ) ↔ (x ∈ A ∧ (y ∈ B ∧ φ)))
6	5	exbii 1582	. . . . . 6 ⊢ (∃y(x ∈ A ∧ y ∈ B ∧ φ) ↔ ∃y(x ∈ A ∧ (y ∈ B ∧ φ)))
7		19.42v 1905	. . . . . 6 ⊢ (∃y(x ∈ A ∧ (y ∈ B ∧ φ)) ↔ (x ∈ A ∧ ∃y(y ∈ B ∧ φ)))
8		df-rex 2621	. . . . . . . 8 ⊢ (∃y ∈ B φ ↔ ∃y(y ∈ B ∧ φ))
9	8	bicomi 193	. . . . . . 7 ⊢ (∃y(y ∈ B ∧ φ) ↔ ∃y ∈ B φ)
10	9	anbi2i 675	. . . . . 6 ⊢ ((x ∈ A ∧ ∃y(y ∈ B ∧ φ)) ↔ (x ∈ A ∧ ∃y ∈ B φ))
11	6, 7, 10	3bitri 262	. . . . 5 ⊢ (∃y(x ∈ A ∧ y ∈ B ∧ φ) ↔ (x ∈ A ∧ ∃y ∈ B φ))
12	11	exbii 1582	. . . 4 ⊢ (∃x∃y(x ∈ A ∧ y ∈ B ∧ φ) ↔ ∃x(x ∈ A ∧ ∃y ∈ B φ))
13		df-rex 2621	. . . 4 ⊢ (∃x ∈ A ∃y ∈ B φ ↔ ∃x(x ∈ A ∧ ∃y ∈ B φ))
14	12, 13	bitr4i 243	. . 3 ⊢ (∃x∃y(x ∈ A ∧ y ∈ B ∧ φ) ↔ ∃x ∈ A ∃y ∈ B φ)
15		3anan12 947	. . . . . . . . . . 11 ⊢ ((x ∈ A ∧ y ∈ B ∧ φ) ↔ (y ∈ B ∧ (x ∈ A ∧ φ)))
16	15	imbi1i 315	. . . . . . . . . 10 ⊢ (((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ ((y ∈ B ∧ (x ∈ A ∧ φ)) → (x = z ∧ y = w)))
17		impexp 433	. . . . . . . . . 10 ⊢ (((y ∈ B ∧ (x ∈ A ∧ φ)) → (x = z ∧ y = w)) ↔ (y ∈ B → ((x ∈ A ∧ φ) → (x = z ∧ y = w))))
18		impexp 433	. . . . . . . . . . 11 ⊢ (((x ∈ A ∧ φ) → (x = z ∧ y = w)) ↔ (x ∈ A → (φ → (x = z ∧ y = w))))
19	18	imbi2i 303	. . . . . . . . . 10 ⊢ ((y ∈ B → ((x ∈ A ∧ φ) → (x = z ∧ y = w))) ↔ (y ∈ B → (x ∈ A → (φ → (x = z ∧ y = w)))))
20	16, 17, 19	3bitri 262	. . . . . . . . 9 ⊢ (((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ (y ∈ B → (x ∈ A → (φ → (x = z ∧ y = w)))))
21	20	albii 1566	. . . . . . . 8 ⊢ (∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ ∀y(y ∈ B → (x ∈ A → (φ → (x = z ∧ y = w)))))
22		df-ral 2620	. . . . . . . 8 ⊢ (∀y ∈ B (x ∈ A → (φ → (x = z ∧ y = w))) ↔ ∀y(y ∈ B → (x ∈ A → (φ → (x = z ∧ y = w)))))
23		r19.21v 2702	. . . . . . . 8 ⊢ (∀y ∈ B (x ∈ A → (φ → (x = z ∧ y = w))) ↔ (x ∈ A → ∀y ∈ B (φ → (x = z ∧ y = w))))
24	21, 22, 23	3bitr2i 264	. . . . . . 7 ⊢ (∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ (x ∈ A → ∀y ∈ B (φ → (x = z ∧ y = w))))
25	24	albii 1566	. . . . . 6 ⊢ (∀x∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ ∀x(x ∈ A → ∀y ∈ B (φ → (x = z ∧ y = w))))
26		df-ral 2620	. . . . . 6 ⊢ (∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)) ↔ ∀x(x ∈ A → ∀y ∈ B (φ → (x = z ∧ y = w))))
27	25, 26	bitr4i 243	. . . . 5 ⊢ (∀x∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ ∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)))
28	27	exbii 1582	. . . 4 ⊢ (∃w∀x∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ ∃w∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)))
29	28	exbii 1582	. . 3 ⊢ (∃z∃w∀x∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w)) ↔ ∃z∃w∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w)))
30	14, 29	anbi12i 678	. 2 ⊢ ((∃x∃y(x ∈ A ∧ y ∈ B ∧ φ) ∧ ∃z∃w∀x∀y((x ∈ A ∧ y ∈ B ∧ φ) → (x = z ∧ y = w))) ↔ (∃x ∈ A ∃y ∈ B φ ∧ ∃z∃w∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))))
31	3, 4, 30	3bitri 262	1 ⊢ ((∃!x ∈ A ∃!y ∈ B φ ∧ ∀x ∈ A ∃*y ∈ B φ) ↔ (∃x ∈ A ∃y ∈ B φ ∧ ∃z∃w∀x ∈ A ∀y ∈ B (φ → (x = z ∧ y = w))))

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   ∧ w3a 934  ∀wal 1540  ∃wex 1541   ∈ wcel 1710  ∃!weu 2204  ∃*wmo 2205  ∀wral 2615  ∃wrex 2616  ∃!wreu 2617  ∃*wrmo 2618

This theorem was proved from 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

This theorem 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-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623

This theorem is referenced by:  2reu5  3045