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 ⊢ Ⅎ _ y A
ralcomf.2 ⊢ Ⅎ _ x B
Assertion rexcomf ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ y ∈ B ∃ x ∈ A φ

Proof

Step Hyp Ref Expression
1 ralcomf.1 ⊢ Ⅎ _ y A
2 ralcomf.2 ⊢ Ⅎ _ x B
3 ancom ⊢ x ∈ A ∧ y ∈ B ↔ y ∈ B ∧ x ∈ A
4 3 anbi1i ⊢ x ∈ A ∧ y ∈ B ∧ φ ↔ y ∈ B ∧ x ∈ A ∧ φ
5 4 2exbii ⊢ ∃ x ∃ y x ∈ A ∧ y ∈ B ∧ φ ↔ ∃ x ∃ y y ∈ B ∧ x ∈ A ∧ φ
6 excom ⊢ ∃ x ∃ y y ∈ B ∧ x ∈ A ∧ φ ↔ ∃ y ∃ x y ∈ B ∧ x ∈ A ∧ φ
7 5 6 bitri ⊢ ∃ x ∃ y x ∈ A ∧ y ∈ B ∧ φ ↔ ∃ y ∃ x y ∈ B ∧ x ∈ A ∧ φ
8 1 r2exf ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ x ∃ y x ∈ A ∧ y ∈ B ∧ φ
9 2 r2exf ⊢ ∃ y ∈ B ∃ x ∈ A φ ↔ ∃ y ∃ x y ∈ B ∧ x ∈ A ∧ φ
10 7 8 9 3bitr4i ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ y ∈ B ∃ x ∈ A φ