Theorem riota2df

Description: A deduction version of riota2f . (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 15-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		riota2df.1	|- F/ x ph
2		riota2df.2	|- ( ph -> F/_ x B )
3		riota2df.3	|- ( ph -> F/ x ch )
4		riota2df.4	|- ( ph -> B e. A )
5		riota2df.5	|- ( ( ph /\ x = B ) -> ( ps <-> ch ) )
6	4	adantr	|- ( ( ph /\ E! x e. A ps ) -> B e. A )
7		simpr	|- ( ( ph /\ E! x e. A ps ) -> E! x e. A ps )
8		df-reu	|- ( E! x e. A ps <-> E! x ( x e. A /\ ps ) )
9	7 8	sylib	|- ( ( ph /\ E! x e. A ps ) -> E! x ( x e. A /\ ps ) )
10		simpr	|- ( ( ( ph /\ E! x e. A ps ) /\ x = B ) -> x = B )
11	6	adantr	|- ( ( ( ph /\ E! x e. A ps ) /\ x = B ) -> B e. A )
12	10 11	eqeltrd	|- ( ( ( ph /\ E! x e. A ps ) /\ x = B ) -> x e. A )
13	12	biantrurd	|- ( ( ( ph /\ E! x e. A ps ) /\ x = B ) -> ( ps <-> ( x e. A /\ ps ) ) )
14	5	adantlr	|- ( ( ( ph /\ E! x e. A ps ) /\ x = B ) -> ( ps <-> ch ) )
15	13 14	bitr3d	|- ( ( ( ph /\ E! x e. A ps ) /\ x = B ) -> ( ( x e. A /\ ps ) <-> ch ) )
16		nfreu1	|- F/ x E! x e. A ps
17	1 16	nfan	|- F/ x ( ph /\ E! x e. A ps )
18	3	adantr	|- ( ( ph /\ E! x e. A ps ) -> F/ x ch )
19	2	adantr	|- ( ( ph /\ E! x e. A ps ) -> F/_ x B )
20	6 9 15 17 18 19	iota2df	|- ( ( ph /\ E! x e. A ps ) -> ( ch <-> ( iota x ( x e. A /\ ps ) ) = B ) )
21		df-riota	|- ( iota_ x e. A ps ) = ( iota x ( x e. A /\ ps ) )
22	21	eqeq1i	|- ( ( iota_ x e. A ps ) = B <-> ( iota x ( x e. A /\ ps ) ) = B )
23	20 22	bitr4di	|- ( ( ph /\ E! x e. A ps ) -> ( ch <-> ( iota_ x e. A ps ) = B ) )