Theorem axsepg2

Description: A generalization of ax-sep in which y and z need not be distinct. See also axsepg which instead allows z to occur in ph . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BTernaryTau, 3-Aug-2025) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑧
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	biimpd	⊢ ( 𝑤 = 𝑦 → ( ( 𝑥 ∈ 𝑤 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
13	12	alimdv	⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
14	13	a1i	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( 𝑤 = 𝑦 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) ) )
15		elequ2	⊢ ( 𝑦 = 𝑧 → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧 ) )
16	15	anbi1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
17	16	bibi2d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
18	17	biimpd	⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
19	18	alimdv	⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
20	19	sps	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
21		ax-sep	⊢ ∃ 𝑤 ∀ 𝑥 ( 𝑥 ∈ 𝑤 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
22		ax-nul	⊢ ∃ 𝑦 ∀ 𝑥 ¬ 𝑥 ∈ 𝑦
23		id	⊢ ( ¬ 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ 𝑦 )
24	23	bianfd	⊢ ( ¬ 𝑥 ∈ 𝑦 → ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
25	24	alimi	⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑦 → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
26	22 25	eximii	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) )
27	8 9 14 20 21 26	dvelimexcasei	⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )