Theorem 2reuswap 1933

Description: A condition allowing swap of uniqueness and existential quantifiers.

Assertion

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

Distinct variable group:   x,y,A

Proof of Theorem 2reuswap

Step	Hyp	Ref	Expression
1		df-ral 1646	. . 3 ⊢ (∀x ∈ A ∃*y(y ∈ A ⋀ φ) ↔ ∀x(x ∈ A → ∃*y(y ∈ A ⋀ φ)))
2		moanimv 1427	. . . 4 ⊢ (∃*y(x ∈ A ⋀ (y ∈ A ⋀ φ)) ↔ (x ∈ A → ∃*y(y ∈ A ⋀ φ)))
3	2	albii 997	. . 3 ⊢ (∀x∃*y(x ∈ A ⋀ (y ∈ A ⋀ φ)) ↔ ∀x(x ∈ A → ∃*y(y ∈ A ⋀ φ)))
4	1, 3	bitr4 176	. 2 ⊢ (∀x ∈ A ∃*y(y ∈ A ⋀ φ) ↔ ∀x∃*y(x ∈ A ⋀ (y ∈ A ⋀ φ)))
5		2euswap 1443	. . 3 ⊢ (∀x∃*y(x ∈ A ⋀ (y ∈ A ⋀ φ)) → (∃!x∃y(x ∈ A ⋀ (y ∈ A ⋀ φ)) → ∃!y∃x(x ∈ A ⋀ (y ∈ A ⋀ φ))))
6		df-reu 1648	. . . 4 ⊢ (∃!x ∈ A ∃y ∈ A φ ↔ ∃!x(x ∈ A ⋀ ∃y ∈ A φ))
7		df-rex 1647	. . . . . 6 ⊢ (∃y ∈ A (x ∈ A ⋀ φ) ↔ ∃y(y ∈ A ⋀ (x ∈ A ⋀ φ)))
8		r19.42v 1761	. . . . . 6 ⊢ (∃y ∈ A (x ∈ A ⋀ φ) ↔ (x ∈ A ⋀ ∃y ∈ A φ))
9		an12 484	. . . . . . 7 ⊢ ((y ∈ A ⋀ (x ∈ A ⋀ φ)) ↔ (x ∈ A ⋀ (y ∈ A ⋀ φ)))
10	9	exbii 1049	. . . . . 6 ⊢ (∃y(y ∈ A ⋀ (x ∈ A ⋀ φ)) ↔ ∃y(x ∈ A ⋀ (y ∈ A ⋀ φ)))
11	7, 8, 10	3bitr3 181	. . . . 5 ⊢ ((x ∈ A ⋀ ∃y ∈ A φ) ↔ ∃y(x ∈ A ⋀ (y ∈ A ⋀ φ)))
12	11	eubii 1385	. . . 4 ⊢ (∃!x(x ∈ A ⋀ ∃y ∈ A φ) ↔ ∃!x∃y(x ∈ A ⋀ (y ∈ A ⋀ φ)))
13	6, 12	bitr 173	. . 3 ⊢ (∃!x ∈ A ∃y ∈ A φ ↔ ∃!x∃y(x ∈ A ⋀ (y ∈ A ⋀ φ)))
14		df-reu 1648	. . . 4 ⊢ (∃!y ∈ A ∃x ∈ A φ ↔ ∃!y(y ∈ A ⋀ ∃x ∈ A φ))
15		r19.42v 1761	. . . . . 6 ⊢ (∃x ∈ A (y ∈ A ⋀ φ) ↔ (y ∈ A ⋀ ∃x ∈ A φ))
16		df-rex 1647	. . . . . 6 ⊢ (∃x ∈ A (y ∈ A ⋀ φ) ↔ ∃x(x ∈ A ⋀ (y ∈ A ⋀ φ)))
17	15, 16	bitr3 175	. . . . 5 ⊢ ((y ∈ A ⋀ ∃x ∈ A φ) ↔ ∃x(x ∈ A ⋀ (y ∈ A ⋀ φ)))
18	17	eubii 1385	. . . 4 ⊢ (∃!y(y ∈ A ⋀ ∃x ∈ A φ) ↔ ∃!y∃x(x ∈ A ⋀ (y ∈ A ⋀ φ)))
19	14, 18	bitr 173	. . 3 ⊢ (∃!y ∈ A ∃x ∈ A φ ↔ ∃!y∃x(x ∈ A ⋀ (y ∈ A ⋀ φ)))
20	5, 13, 19	3imtr4g 552	. 2 ⊢ (∀x∃*y(x ∈ A ⋀ (y ∈ A ⋀ φ)) → (∃!x ∈ A ∃y ∈ A φ → ∃!y ∈ A ∃x ∈ A φ))
21	4, 20	sylbi 199	1 ⊢ (∀x ∈ A ∃*y(y ∈ A ⋀ φ) → (∃!x ∈ A ∃y ∈ A φ → ∃!y ∈ A ∃x ∈ A φ))

Syntax hints:   → wi 3   ⋀ wa 223  ∀wal 952   ∈ wcel 956  ∃wex 978  ∃!weu 1378  ∃*wmo 1379  ∀wral 1642  ∃wrex 1643  ∃!wreu 1644

This theorem is referenced by:  reuxfr2 2902

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-ral 1646  df-rex 1647  df-reu 1648

Copyright terms: Public domain