This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iotaex

Description: Theorem 8.23 in Quine p. 58. This theorem proves the existence of the iota class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011) Remove dependency on ax-10 , ax-11 , ax-12 . (Revised by SN, 6-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		iotaval2	\|- ( { 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		iotanul2	\|- ( -. 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