Metamath Proof Explorer

Theorem axsepg2ALT

Description: Alternate proof of axsepg2 , derived directly from ax-sep with no additional set theory axioms. (Contributed by BTernaryTau, 3-Aug-2025) (Proof modification is discouraged.) (New usage is discouraged.)

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

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-sep ⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑣 ∧ ⊥ ) )
23 fal ⊢ ¬ ⊥
24 23 intnan ⊢ ¬ ( 𝑥 ∈ 𝑣 ∧ ⊥ )
25 biimp ⊢ ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑣 ∧ ⊥ ) ) → ( 𝑥 ∈ 𝑦 → ( 𝑥 ∈ 𝑣 ∧ ⊥ ) ) )
26 24 25 mtoi ⊢ ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑣 ∧ ⊥ ) ) → ¬ 𝑥 ∈ 𝑦 )
27 26 bianfd ⊢ ( ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑣 ∧ ⊥ ) ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
28 27 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑣 ∧ ⊥ ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) ) )
29 22 28 eximii ⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑦 ∧ 𝜑 ) )
30 8 9 14 20 21 29 dvelimexcasei ⊢ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )