Theorem axsepg5

Description: A generalization of ax-sep that combines axsepg , axsepg2 , and axsepg3 into a single theorem scheme. Unlike ax-sep , this scheme lacks a distinct variable condition for ph and z , for x and z , and for y and z . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BTernaryTau, 24-May-2026) (New usage is discouraged.)

	Ref	Expression
Assertion	axsepg5	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nfnae	⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑧
2		nfvd	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 𝑥 ∈ 𝑤 )
3		nfcvf	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 𝑧 )
4	3	nfcrd	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 𝑥 ∈ 𝑧 )
5		nfvd	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 𝜑 )
6	4 5	nfand	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
7	2 6	nfbid	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 ( 𝑥 ∈ 𝑤 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
8	1 7	nfald	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
9		nfvd	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑤 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
10		elequ2	⊢ ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) )
11	10	bibi1d	⊢ ( 𝑤 = 𝑦 → ( ( 𝑥 ∈ 𝑤 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
12	11	albidv	⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
13	12	biimpd	⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
14	13	a1i	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( 𝑤 = 𝑦 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) ) )
15		nfae	⊢ Ⅎ 𝑥 ∀ 𝑦 𝑦 = 𝑧
16		elequ2	⊢ ( 𝑦 = 𝑧 → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧 ) )
17	16	anbi1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
18	17	bibi2d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
19	18	biimpd	⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
20	19	sps	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
21	15 20	alimd	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
22		axsepg4	⊢ ∃ 𝑤 ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
23		axsepg3	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) )
24	8 9 14 21 22 23	dvelimexcasei	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )