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 ⊢ ∃ y ∀ x x ∈ y ↔ x ∈ z ∧ φ

Proof

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