Metamath Proof Explorer

Theorem sn-exelALT

Description: Alternate proof of exel , avoiding ax-pr but requiring ax-5 , ax-9 , and ax-pow . This is similar to how elALT2 uses ax-pow instead of ax-pr compared to el . (Contributed by SN, 18-Sep-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sn-exelALT ⊢ ∃ y ∃ x x ∈ y

Proof

Step Hyp Ref Expression
1 ax-pow ⊢ ∃ y ∀ x ∀ w w ∈ x → w ∈ z → x ∈ y
2 ax6ev ⊢ ∃ x x = z
3 ax9v1 ⊢ x = z → w ∈ x → w ∈ z
4 3 alrimiv ⊢ x = z → ∀ w w ∈ x → w ∈ z
5 2 4 eximii ⊢ ∃ x ∀ w w ∈ x → w ∈ z
6 exim ⊢ ∀ x ∀ w w ∈ x → w ∈ z → x ∈ y → ∃ x ∀ w w ∈ x → w ∈ z → ∃ x x ∈ y
7 5 6 mpi ⊢ ∀ x ∀ w w ∈ x → w ∈ z → x ∈ y → ∃ x x ∈ y
8 1 7 eximii ⊢ ∃ y ∃ x x ∈ y