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	$⊢ \underline{Ⅎ} y A$
		ralcomf.2	$⊢ \underline{Ⅎ} x B$
	Assertion	rexcomf	$⊢ \exists x \in A \exists y \in B φ \leftrightarrow \exists y \in B \exists x \in A φ$

Proof

Step	Hyp	Ref	Expression
1		ralcomf.1	$⊢ \underline{Ⅎ} y A$
2		ralcomf.2	$⊢ \underline{Ⅎ} x B$
3		ancom	$⊢ (x \in A \land y \in B) \leftrightarrow (y \in B \land x \in A)$
4	3	anbi1i	$⊢ ((x \in A \land y \in B) \land φ) \leftrightarrow ((y \in B \land x \in A) \land φ)$
5	4	2exbii	$⊢ \exists x \exists y ((x \in A \land y \in B) \land φ) \leftrightarrow \exists x \exists y ((y \in B \land x \in A) \land φ)$
6		excom	$⊢ \exists x \exists y ((y \in B \land x \in A) \land φ) \leftrightarrow \exists y \exists x ((y \in B \land x \in A) \land φ)$
7	5 6	bitri	$⊢ \exists x \exists y ((x \in A \land y \in B) \land φ) \leftrightarrow \exists y \exists x ((y \in B \land x \in A) \land φ)$
8	1	r2exf	$⊢ \exists x \in A \exists y \in B φ \leftrightarrow \exists x \exists y ((x \in A \land y \in B) \land φ)$
9	2	r2exf	$⊢ \exists y \in B \exists x \in A φ \leftrightarrow \exists y \exists x ((y \in B \land x \in A) \land φ)$
10	7 8 9	3bitr4i	$⊢ \exists x \in A \exists y \in B φ \leftrightarrow \exists y \in B \exists x \in A φ$