Theorem 2reuswap 3039

Description: A condition allowing swap of uniqueness and existential quantifiers. (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by NM, 16-Jun-2017.)

Assertion

Ref	Expression
2reuswap	⊢ (∀x ∈ A ∃*y ∈ B φ → (∃!x ∈ A ∃y ∈ B φ → ∃!y ∈ B ∃x ∈ A φ))

Distinct variable groups:   x,y,A   x,B

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

Proof of Theorem 2reuswap

Step	Hyp	Ref	Expression
1		df-rmo 2623	. . 3 ⊢ (∃*y ∈ B φ ↔ ∃*y(y ∈ B ∧ φ))
2	1	ralbii 2639	. 2 ⊢ (∀x ∈ A ∃*y ∈ B φ ↔ ∀x ∈ A ∃*y(y ∈ B ∧ φ))
3		df-ral 2620	. . . 4 ⊢ (∀x ∈ A ∃*y(y ∈ B ∧ φ) ↔ ∀x(x ∈ A → ∃*y(y ∈ B ∧ φ)))
4		moanimv 2262	. . . . 5 ⊢ (∃*y(x ∈ A ∧ (y ∈ B ∧ φ)) ↔ (x ∈ A → ∃*y(y ∈ B ∧ φ)))
5	4	albii 1566	. . . 4 ⊢ (∀x∃*y(x ∈ A ∧ (y ∈ B ∧ φ)) ↔ ∀x(x ∈ A → ∃*y(y ∈ B ∧ φ)))
6	3, 5	bitr4i 243	. . 3 ⊢ (∀x ∈ A ∃*y(y ∈ B ∧ φ) ↔ ∀x∃*y(x ∈ A ∧ (y ∈ B ∧ φ)))
7		2euswap 2280	. . . 4 ⊢ (∀x∃*y(x ∈ A ∧ (y ∈ B ∧ φ)) → (∃!x∃y(x ∈ A ∧ (y ∈ B ∧ φ)) → ∃!y∃x(x ∈ A ∧ (y ∈ B ∧ φ))))
8		df-reu 2622	. . . . 5 ⊢ (∃!x ∈ A ∃y ∈ B φ ↔ ∃!x(x ∈ A ∧ ∃y ∈ B φ))
9		r19.42v 2766	. . . . . . . 8 ⊢ (∃y ∈ B (x ∈ A ∧ φ) ↔ (x ∈ A ∧ ∃y ∈ B φ))
10		df-rex 2621	. . . . . . . 8 ⊢ (∃y ∈ B (x ∈ A ∧ φ) ↔ ∃y(y ∈ B ∧ (x ∈ A ∧ φ)))
11	9, 10	bitr3i 242	. . . . . . 7 ⊢ ((x ∈ A ∧ ∃y ∈ B φ) ↔ ∃y(y ∈ B ∧ (x ∈ A ∧ φ)))
12		an12 772	. . . . . . . 8 ⊢ ((y ∈ B ∧ (x ∈ A ∧ φ)) ↔ (x ∈ A ∧ (y ∈ B ∧ φ)))
13	12	exbii 1582	. . . . . . 7 ⊢ (∃y(y ∈ B ∧ (x ∈ A ∧ φ)) ↔ ∃y(x ∈ A ∧ (y ∈ B ∧ φ)))
14	11, 13	bitri 240	. . . . . 6 ⊢ ((x ∈ A ∧ ∃y ∈ B φ) ↔ ∃y(x ∈ A ∧ (y ∈ B ∧ φ)))
15	14	eubii 2213	. . . . 5 ⊢ (∃!x(x ∈ A ∧ ∃y ∈ B φ) ↔ ∃!x∃y(x ∈ A ∧ (y ∈ B ∧ φ)))
16	8, 15	bitri 240	. . . 4 ⊢ (∃!x ∈ A ∃y ∈ B φ ↔ ∃!x∃y(x ∈ A ∧ (y ∈ B ∧ φ)))
17		df-reu 2622	. . . . 5 ⊢ (∃!y ∈ B ∃x ∈ A φ ↔ ∃!y(y ∈ B ∧ ∃x ∈ A φ))
18		r19.42v 2766	. . . . . . 7 ⊢ (∃x ∈ A (y ∈ B ∧ φ) ↔ (y ∈ B ∧ ∃x ∈ A φ))
19		df-rex 2621	. . . . . . 7 ⊢ (∃x ∈ A (y ∈ B ∧ φ) ↔ ∃x(x ∈ A ∧ (y ∈ B ∧ φ)))
20	18, 19	bitr3i 242	. . . . . 6 ⊢ ((y ∈ B ∧ ∃x ∈ A φ) ↔ ∃x(x ∈ A ∧ (y ∈ B ∧ φ)))
21	20	eubii 2213	. . . . 5 ⊢ (∃!y(y ∈ B ∧ ∃x ∈ A φ) ↔ ∃!y∃x(x ∈ A ∧ (y ∈ B ∧ φ)))
22	17, 21	bitri 240	. . . 4 ⊢ (∃!y ∈ B ∃x ∈ A φ ↔ ∃!y∃x(x ∈ A ∧ (y ∈ B ∧ φ)))
23	7, 16, 22	3imtr4g 261	. . 3 ⊢ (∀x∃*y(x ∈ A ∧ (y ∈ B ∧ φ)) → (∃!x ∈ A ∃y ∈ B φ → ∃!y ∈ B ∃x ∈ A φ))
24	6, 23	sylbi 187	. 2 ⊢ (∀x ∈ A ∃*y(y ∈ B ∧ φ) → (∃!x ∈ A ∃y ∈ B φ → ∃!y ∈ B ∃x ∈ A φ))
25	2, 24	sylbi 187	1 ⊢ (∀x ∈ A ∃*y ∈ B φ → (∃!x ∈ A ∃y ∈ B φ → ∃!y ∈ B ∃x ∈ A φ))

This proof depends on syntax axioms:   → wi 4   ∧ wa 358  ∀wal 1540  ∃wex 1541   ∈ wcel 1710  ∃!weu 2204  ∃*wmo 2205  ∀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

This proof depends on definitions:  df-bi 177  df-or 359  df-an 360  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 used by: (None)