Theorem sn-iotaex

Description: iotaex without ax-10 , ax-11 , ax-12 . (Contributed by SN, 6-Nov-2024)

	Ref	Expression
Assertion	sn-iotaex	|- ( iota x ph ) e. _V

Proof

Step	Hyp	Ref	Expression
1		sn-iotaval	|- ( { x | ph } = { y } -> ( iota x ph ) = y )
2		vex	|- y e. _V
3	1 2	eqeltrdi	|- ( { x | ph } = { y } -> ( iota x ph ) e. _V )
4	3	exlimiv	|- ( E. y { x | ph } = { y } -> ( iota x ph ) e. _V )
5		sn-iotanul	|- ( -. E. y { x | ph } = { y } -> ( iota x ph ) = (/) )
6		0ex	|- (/) e. _V
7	5 6	eqeltrdi	|- ( -. E. y { x | ph } = { y } -> ( iota x ph ) e. _V )
8	4 7	pm2.61i	|- ( iota x ph ) e. _V