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