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