Metamath Proof Explorer

Theorem axsepg3

Description: A generalization of ax-sep in which y and z need not be distinct. This theorem scheme bundles ax-sep with the degenerate instance E. y A. x ( x e. y <-> ( x e. y /\ ph ) ) which is satisfied by the existence of the empty set. 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 axsepg3 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )

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