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

Metamath Proof Explorer

Theorem rexcom4b

Description: Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011)

Ref Expression
Hypothesis rexcom4b.1 ⊢ B ∈ V
Assertion rexcom4b ⊢ ∃ x ∃ y ∈ A φ ∧ x = B ↔ ∃ y ∈ A φ

Proof

Step Hyp Ref Expression
1 rexcom4b.1 ⊢ B ∈ V
2 rexcom4a ⊢ ∃ x ∃ y ∈ A φ ∧ x = B ↔ ∃ y ∈ A φ ∧ ∃ x x = B
3 1 isseti ⊢ ∃ x x = B
4 3 biantru ⊢ φ ↔ φ ∧ ∃ x x = B
5 4 rexbii ⊢ ∃ y ∈ A φ ↔ ∃ y ∈ A φ ∧ ∃ x x = B
6 2 5 bitr4i ⊢ ∃ x ∃ y ∈ A φ ∧ x = B ↔ ∃ y ∈ A φ