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

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 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 elequ2 ⊢ ( 𝑤 = 𝑧 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑧 ) )
2 1 anbi1d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
3 2 bibi2d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
4 3 albidv ⊢ ( 𝑤 = 𝑧 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
5 4 exbidv ⊢ ( 𝑤 = 𝑧 → ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
6 ax-sep ⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
7 5 6 chvarvv ⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )