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)

	Ref	Expression
Hypothesis	iotan0.1	|- ( x = A -> ( ph <-> ps ) )
Assertion	iotan0	|- ( ( A e. V /\ 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	a1i	|- ( A e. V -> ( A =/= (/) -> ( A = ( iota x ph ) -> E! x ph ) ) )
8	7	3imp	|- ( ( A e. V /\ A =/= (/) /\ A = ( iota x ph ) ) -> E! x ph )
9		eqcom	|- ( A = ( iota x ph ) <-> ( iota x ph ) = A )
10	1	iota2	|- ( ( A e. V /\ E! x ph ) -> ( ps <-> ( iota x ph ) = A ) )
11	10	biimprd	|- ( ( A e. V /\ E! x ph ) -> ( ( iota x ph ) = A -> ps ) )
12	9 11	syl5bi	|- ( ( A e. V /\ E! x ph ) -> ( A = ( iota x ph ) -> ps ) )
13	12	impancom	|- ( ( A e. V /\ A = ( iota x ph ) ) -> ( E! x ph -> ps ) )
14	13	3adant2	|- ( ( A e. V /\ A =/= (/) /\ A = ( iota x ph ) ) -> ( E! x ph -> ps ) )
15	8 14	mpd	|- ( ( A e. V /\ A =/= (/) /\ A = ( iota x ph ) ) -> ps )