Metamath Proof Explorer

Theorem axsepg

Description: A more general version of the axiom scheme of separation ax-sep , where variable z can also occur (in addition to x ) in formula ph , which can therefore be thought of as ph ( x , z ) . This version is derived from the more restrictive ax-sep with no additional set theory axioms. Note that it was also derived from ax-rep but without ax-sep as axsepgfromrep . (Contributed by NM, 10-Dec-2006) (Proof shortened by Mario Carneiro, 17-Nov-2016) Remove dependency on ax-12 and ax-13 and shorten proof. (Revised by BJ, 6-Oct-2019)

Ref Expression
Assertion axsepg ⊢ ∃ y ∀ x x ∈ y ↔ x ∈ z ∧ φ

Proof

Step Hyp Ref Expression
1 elequ2 ⊢ w = z → x ∈ w ↔ x ∈ z
2 1 anbi1d ⊢ w = z → x ∈ w ∧ φ ↔ x ∈ z ∧ φ
3 2 bibi2d ⊢ w = z → x ∈ y ↔ x ∈ w ∧ φ ↔ x ∈ y ↔ x ∈ z ∧ φ
4 3 albidv ⊢ w = z → ∀ x x ∈ y ↔ x ∈ w ∧ φ ↔ ∀ x x ∈ y ↔ x ∈ z ∧ φ
5 4 exbidv ⊢ w = z → ∃ y ∀ x x ∈ y ↔ x ∈ w ∧ φ ↔ ∃ y ∀ x x ∈ y ↔ x ∈ z ∧ φ
6 ax-sep ⊢ ∃ y ∀ x x ∈ y ↔ x ∈ w ∧ φ
7 5 6 chvarvv ⊢ ∃ y ∀ x x ∈ y ↔ x ∈ z ∧ φ