This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )