This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rexcomf

Description: Commutation of restricted existential quantifiers. For a version based on fewer axioms see rexcom . (Contributed by Mario Carneiro, 14-Oct-2016)

		Ref	Expression
	Hypotheses	ralcomf.1	⊢ Ⅎ 𝑦 𝐴
		ralcomf.2	⊢ Ⅎ 𝑥 𝐵
	Assertion	rexcomf	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ralcomf.1	⊢ Ⅎ 𝑦 𝐴
2		ralcomf.2	⊢ Ⅎ 𝑥 𝐵
3		ancom	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
4	3	anbi1i	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜑 ) )
5	4	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜑 ) )
6		excom	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜑 ) )
7	5 6	bitri	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜑 ) )
8	1	r2exf	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) )
9	2	r2exf	⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜑 ) )
10	7 8 9	3bitr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 )