Theorem riota2f

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

	Ref	Expression
Hypotheses	riota2f.1	|- F/_ x B
	riota2f.2	|- F/ x ps
	riota2f.3	|- ( x = B -> ( ph <-> ps ) )
Assertion	riota2f	|- ( ( B e. A /\ E! x e. A ph ) -> ( ps <-> ( iota_ x e. A ph ) = B ) )

Proof

Step	Hyp	Ref	Expression
1		riota2f.1	|- F/_ x B
2		riota2f.2	|- F/ x ps
3		riota2f.3	|- ( x = B -> ( ph <-> ps ) )
4	1	nfel1	|- F/ x B e. A
5	1	a1i	|- ( B e. A -> F/_ x B )
6	2	a1i	|- ( B e. A -> F/ x ps )
7		id	|- ( B e. A -> B e. A )
8	3	adantl	|- ( ( B e. A /\ x = B ) -> ( ph <-> ps ) )
9	4 5 6 7 8	riota2df	|- ( ( B e. A /\ E! x e. A ph ) -> ( ps <-> ( iota_ x e. A ph ) = B ) )