Theorem iota2df

Description: A condition that allows us to represent "the unique element such that ph " with a class expression A . (Contributed by NM, 30-Dec-2014)

	Ref	Expression
Hypotheses	iota2df.1	|- ( ph -> B e. V )
	iota2df.2	|- ( ph -> E! x ps )
	iota2df.3	|- ( ( ph /\ x = B ) -> ( ps <-> ch ) )
	iota2df.4	|- F/ x ph
	iota2df.5	|- ( ph -> F/ x ch )
	iota2df.6	|- ( ph -> F/_ x B )
Assertion	iota2df	|- ( ph -> ( ch <-> ( iota x ps ) = B ) )

Proof

Step	Hyp	Ref	Expression
1		iota2df.1	|- ( ph -> B e. V )
2		iota2df.2	|- ( ph -> E! x ps )
3		iota2df.3	|- ( ( ph /\ x = B ) -> ( ps <-> ch ) )
4		iota2df.4	|- F/ x ph
5		iota2df.5	|- ( ph -> F/ x ch )
6		iota2df.6	|- ( ph -> F/_ x B )
7		simpr	|- ( ( ph /\ x = B ) -> x = B )
8	7	eqeq2d	|- ( ( ph /\ x = B ) -> ( ( iota x ps ) = x <-> ( iota x ps ) = B ) )
9	3 8	bibi12d	|- ( ( ph /\ x = B ) -> ( ( ps <-> ( iota x ps ) = x ) <-> ( ch <-> ( iota x ps ) = B ) ) )
10		iota1	|- ( E! x ps -> ( ps <-> ( iota x ps ) = x ) )
11	2 10	syl	|- ( ph -> ( ps <-> ( iota x ps ) = x ) )
12		nfiota1	|- F/_ x ( iota x ps )
13	12	a1i	|- ( ph -> F/_ x ( iota x ps ) )
14	13 6	nfeqd	|- ( ph -> F/ x ( iota x ps ) = B )
15	5 14	nfbid	|- ( ph -> F/ x ( ch <-> ( iota x ps ) = B ) )
16	1 9 11 4 6 15	vtocldf	|- ( ph -> ( ch <-> ( iota x ps ) = B ) )