Theorem iota2d

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 ) )
Assertion	iota2d	|- ( 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		nfv	|- F/ x ph
5		nfvd	|- ( ph -> F/ x ch )
6		nfcvd	|- ( ph -> F/_ x B )
7	1 2 3 4 5 6	iota2df	|- ( ph -> ( ch <-> ( iota x ps ) = B ) )