Theorem riota2

Description: This theorem shows a condition that allows us to represent a descriptor with a class expression B . (Contributed by NM, 23-Aug-2011) (Revised by Mario Carneiro, 10-Dec-2016)

	Ref	Expression
Hypothesis	riota2.1	|- ( x = B -> ( ph <-> ps ) )
Assertion	riota2	|- ( ( B e. A /\ E! x e. A ph ) -> ( ps <-> ( iota_ x e. A ph ) = B ) )

Proof

Step	Hyp	Ref	Expression
1		riota2.1	|- ( x = B -> ( ph <-> ps ) )
2		nfcv	|- F/_ x B
3		nfv	|- F/ x ps
4	2 3 1	riota2f	|- ( ( B e. A /\ E! x e. A ph ) -> ( ps <-> ( iota_ x e. A ph ) = B ) )