Metamath Proof Explorer

Theorem axsepg4

Description: A generalization of ax-sep that combines axsepg and axsepg2 into a single theorem scheme. Unlike ax-sep , this scheme lacks a distinct variable condition for ph and z as well as for x 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 axsepg4 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 nfa1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
2 1 a1i ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 ∀ 𝑧 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
3 nfvd ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑤 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
4 sp ⊢ ( ∀ 𝑧 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) → ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) )
5 dveeq2 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( 𝑤 = 𝑧 → ∀ 𝑥 𝑤 = 𝑧 ) )
6 5 naecoms ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( 𝑤 = 𝑧 → ∀ 𝑥 𝑤 = 𝑧 ) )
7 elequ2 ⊢ ( 𝑤 = 𝑧 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑧 ) )
8 7 anbi1d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
9 8 bibi2d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
10 9 biimpd ⊢ ( 𝑤 = 𝑧 → ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
11 10 al2imi ⊢ ( ∀ 𝑥 𝑤 = 𝑧 → ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
12 11 eximdv ⊢ ( ∀ 𝑥 𝑤 = 𝑧 → ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) → ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
13 6 12 syl6 ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( 𝑤 = 𝑧 → ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) → ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) ) )
14 4 13 syl7 ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( 𝑤 = 𝑧 → ( ∀ 𝑧 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) ) → ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) ) )
15 elequ1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
16 elequ1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧 ) )
17 16 anbi1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) )
18 15 17 bibi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
19 18 biimpd ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
20 19 al2imi ⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) → ∀ 𝑧 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
21 axc11 ⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑧 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
22 20 21 syld ⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
23 22 eximdv ⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) → ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) ) ) )
24 axsepg ⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
25 24 gen2 ⊢ ∀ 𝑤 ∀ 𝑧 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑤 ∧ 𝜑 ) )
26 ax-nul ⊢ ∃ 𝑦 ∀ 𝑧 ¬ 𝑧 ∈ 𝑦
27 elirrv ⊢ ¬ 𝑧 ∈ 𝑧
28 27 intnanr ⊢ ¬ ( 𝑧 ∈ 𝑧 ∧ 𝜑 )
29 28 nbn ⊢ ( ¬ 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) )
30 29 biimpi ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) )
31 30 alimi ⊢ ( ∀ 𝑧 ¬ 𝑧 ∈ 𝑦 → ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) ) )
32 26 31 eximii ⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) )
33 32 ax-gen ⊢ ∀ 𝑧 ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑧 ∧ 𝜑 ) )
34 2 3 14 23 25 33 dvelimalcasei ⊢ ∀ 𝑧 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )
35 34 spi ⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )