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