Theorem aiotaexim

Description: Representation of "the unique element such that ph " with a class expression A which is a set (that means that "the unique element such that ph " exists). Analog to iotan0 which requires A to be nonempty instead of being a set. That gives a more natural statement, closer to statements like spcgv . (Proposed by BJ, 18-Oct-2026.) (Contributed by AV, 18-Oct-2026)

	Ref	Expression
Hypothesis	aiotaexim.1	|- ( x = A -> ( ph <-> ps ) )
Assertion	aiotaexim	|- ( ( A e. V /\ A = ( iota' x ph ) ) -> ps )

Proof

Step	Hyp	Ref	Expression
1		aiotaexim.1	|- ( x = A -> ( ph <-> ps ) )
2		dfaiota3	|- ( iota' x ph ) = if ( E! x ph , |^| { x | ph } , _V )
3	2	eqeq2i	|- ( A = ( iota' x ph ) <-> A = if ( E! x ph , |^| { x | ph } , _V ) )
4		iftrue	|- ( E! x ph -> if ( E! x ph , |^| { x | ph } , _V ) = |^| { x | ph } )
5	4	eqeq2d	|- ( E! x ph -> ( A = if ( E! x ph , |^| { x | ph } , _V ) <-> A = |^| { x | ph } ) )
6		iotain	|- ( E! x ph -> |^| { x | ph } = ( iota x ph ) )
7	6	eqeq2d	|- ( E! x ph -> ( A = |^| { x | ph } <-> A = ( iota x ph ) ) )
8		eqcom	|- ( A = ( iota x ph ) <-> ( iota x ph ) = A )
9	1	iota2	|- ( ( A e. V /\ E! x ph ) -> ( ps <-> ( iota x ph ) = A ) )
10	9	biimprd	|- ( ( A e. V /\ E! x ph ) -> ( ( iota x ph ) = A -> ps ) )
11	10	expcom	|- ( E! x ph -> ( A e. V -> ( ( iota x ph ) = A -> ps ) ) )
12	11	com23	|- ( E! x ph -> ( ( iota x ph ) = A -> ( A e. V -> ps ) ) )
13	8 12	biimtrid	|- ( E! x ph -> ( A = ( iota x ph ) -> ( A e. V -> ps ) ) )
14	7 13	sylbid	|- ( E! x ph -> ( A = |^| { x | ph } -> ( A e. V -> ps ) ) )
15	5 14	sylbid	|- ( E! x ph -> ( A = if ( E! x ph , |^| { x | ph } , _V ) -> ( A e. V -> ps ) ) )
16		iffalse	|- ( -. E! x ph -> if ( E! x ph , |^| { x | ph } , _V ) = _V )
17	16	eqeq2d	|- ( -. E! x ph -> ( A = if ( E! x ph , |^| { x | ph } , _V ) <-> A = _V ) )
18		nvelim	|- ( A = _V -> -. A e. V )
19	18	pm2.21d	|- ( A = _V -> ( A e. V -> ps ) )
20	17 19	biimtrdi	|- ( -. E! x ph -> ( A = if ( E! x ph , |^| { x | ph } , _V ) -> ( A e. V -> ps ) ) )
21	15 20	pm2.61i	|- ( A = if ( E! x ph , |^| { x | ph } , _V ) -> ( A e. V -> ps ) )
22	3 21	sylbi	|- ( A = ( iota' x ph ) -> ( A e. V -> ps ) )
23	22	impcom	|- ( ( A e. V /\ A = ( iota' x ph ) ) -> ps )