Theorem iotan0

Description: Representation of "the unique element such that ph " with a class expression A which is not the empty set (that means that "the unique element such that ph " exists). (Contributed by AV, 30-Jan-2024) Remove sethood antecedent. (Revised by Eric Schmidt, 17-Oct-2026)

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

Proof

Step	Hyp	Ref	Expression
1		iotan0.1	|- ( x = A -> ( ph <-> ps ) )
2		pm13.18	|- ( ( A = ( iota x ph ) /\ A =/= (/) ) -> ( iota x ph ) =/= (/) )
3	2	expcom	|- ( A =/= (/) -> ( A = ( iota x ph ) -> ( iota x ph ) =/= (/) ) )
4		iotanul	|- ( -. E! x ph -> ( iota x ph ) = (/) )
5	4	necon1ai	|- ( ( iota x ph ) =/= (/) -> E! x ph )
6	3 5	syl6	|- ( A =/= (/) -> ( A = ( iota x ph ) -> E! x ph ) )
7	6	imp	|- ( ( A =/= (/) /\ A = ( iota x ph ) ) -> E! x ph )
8		iotaex	|- ( iota x ph ) e. _V
9		eleq1	|- ( A = ( iota x ph ) -> ( A e. _V <-> ( iota x ph ) e. _V ) )
10	8 9	mpbiri	|- ( A = ( iota x ph ) -> A e. _V )
11		eqcom	|- ( A = ( iota x ph ) <-> ( iota x ph ) = A )
12	1	iota2	|- ( ( A e. _V /\ E! x ph ) -> ( ps <-> ( iota x ph ) = A ) )
13	12	biimprd	|- ( ( A e. _V /\ E! x ph ) -> ( ( iota x ph ) = A -> ps ) )
14	11 13	biimtrid	|- ( ( A e. _V /\ E! x ph ) -> ( A = ( iota x ph ) -> ps ) )
15	14	impancom	|- ( ( A e. _V /\ A = ( iota x ph ) ) -> ( E! x ph -> ps ) )
16	10 15	mpancom	|- ( A = ( iota x ph ) -> ( E! x ph -> ps ) )
17	16	adantl	|- ( ( A =/= (/) /\ A = ( iota x ph ) ) -> ( E! x ph -> ps ) )
18	7 17	mpd	|- ( ( A =/= (/) /\ A = ( iota x ph ) ) -> ps )