Theorem 2reuswap2

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

	Ref	Expression
Assertion	2reuswap2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
2		moanimv	⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
3	2	albii	⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
4	1 3	bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
5		2euswapv	⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) → ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) → ∃! 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ) )
6		df-reu	⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) )
7		r19.42v	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) )
8		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
9	7 8	bitr3i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
10		an12	⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
11	10	exbii	⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
12	9 11	bitri	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
13	12	eubii	⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) ↔ ∃! 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
14	6 13	bitri	⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
15		df-reu	⊢ ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) )
16		r19.42v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) )
17		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
18	16 17	bitr3i	⊢ ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
19	18	eubii	⊢ ( ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ∃! 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
20	15 19	bitri	⊢ ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
21	5 14 20	3imtr4g	⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
22	4 21	sylbi	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )