Metamath Proof Explorer

Theorem sn-axprlem3

Description: axprlem3 using only Tarski's FOL axiom schemes and ax-rep . (Contributed by SN, 22-Sep-2023)

Ref Expression
Assertion sn-axprlem3 ⊢ ∃ y ∀ z z ∈ y ↔ ∃ w ∈ x if- φ z = a z = b

Proof

Step Hyp Ref Expression
1 axrep6 ⊢ ∀ w ∃* z if- φ z = a z = b → ∃ y ∀ z z ∈ y ↔ ∃ w ∈ x if- φ z = a z = b
2 ax6evr ⊢ ∃ y a = y
3 ifptru ⊢ φ → if- φ z = a z = b ↔ z = a
4 3 biimpd ⊢ φ → if- φ z = a z = b → z = a
5 equtrr ⊢ a = y → z = a → z = y
6 4 5 sylan9r ⊢ a = y ∧ φ → if- φ z = a z = b → z = y
7 6 alrimiv ⊢ a = y ∧ φ → ∀ z if- φ z = a z = b → z = y
8 7 expcom ⊢ φ → a = y → ∀ z if- φ z = a z = b → z = y
9 8 eximdv ⊢ φ → ∃ y a = y → ∃ y ∀ z if- φ z = a z = b → z = y
10 2 9 mpi ⊢ φ → ∃ y ∀ z if- φ z = a z = b → z = y
11 ax6evr ⊢ ∃ y b = y
12 ifpfal ⊢ ¬ φ → if- φ z = a z = b ↔ z = b
13 12 biimpd ⊢ ¬ φ → if- φ z = a z = b → z = b
14 equtrr ⊢ b = y → z = b → z = y
15 13 14 sylan9r ⊢ b = y ∧ ¬ φ → if- φ z = a z = b → z = y
16 15 alrimiv ⊢ b = y ∧ ¬ φ → ∀ z if- φ z = a z = b → z = y
17 16 expcom ⊢ ¬ φ → b = y → ∀ z if- φ z = a z = b → z = y
18 17 eximdv ⊢ ¬ φ → ∃ y b = y → ∃ y ∀ z if- φ z = a z = b → z = y
19 11 18 mpi ⊢ ¬ φ → ∃ y ∀ z if- φ z = a z = b → z = y
20 10 19 pm2.61i ⊢ ∃ y ∀ z if- φ z = a z = b → z = y
21 dfmo ⊢ ∃* z if- φ z = a z = b ↔ ∃ y ∀ z if- φ z = a z = b → z = y
22 20 21 mpbir ⊢ ∃* z if- φ z = a z = b
23 1 22 mpg ⊢ ∃ y ∀ z z ∈ y ↔ ∃ w ∈ x if- φ z = a z = b