Metamath Proof Explorer

Theorem riota5f

Description: A method for computing restricted iota. (Contributed by NM, 16-Apr-2013) (Revised by Mario Carneiro, 15-Oct-2016)

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

Proof

Step Hyp Ref Expression
1 riota5f.1 
 |-  ( ph -> F/_ x B )
2 riota5f.2 
 |-  ( ph -> B e. A )
3 riota5f.3 
 |-  ( ( ph /\ x e. A ) -> ( ps <-> x = B ) )
4 3 ralrimiva 
 |-  ( ph -> A. x e. A ( ps <-> x = B ) )
5 trud 
 |-  ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) -> T. )
6 reu6i 
 |-  ( ( y e. A /\ A. x e. A ( ps <-> x = y ) ) -> E! x e. A ps )
7 6 adantl 
 |-  ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) -> E! x e. A ps )
8 nfv 
 |-  F/ x ph
9 nfv 
 |-  F/ x y e. A
10 nfra1 
 |-  F/ x A. x e. A ( ps <-> x = y )
11 9 10 nfan 
 |-  F/ x ( y e. A /\ A. x e. A ( ps <-> x = y ) )
12 8 11 nfan 
 |-  F/ x ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) )
13 nfcvd 
 |-  ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) -> F/_ x y )
14 nfvd 
 |-  ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) -> F/ x T. )
15 simprl 
 |-  ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) -> y e. A )
16 simpr 
 |-  ( ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) /\ x = y ) -> x = y )
17 simplrr 
 |-  ( ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) /\ x = y ) -> A. x e. A ( ps <-> x = y ) )
18 simplrl 
 |-  ( ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) /\ x = y ) -> y e. A )
19 16 18 eqeltrd 
 |-  ( ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) /\ x = y ) -> x e. A )
20 rsp 
 |-  ( A. x e. A ( ps <-> x = y ) -> ( x e. A -> ( ps <-> x = y ) ) )
21 17 19 20 sylc 
 |-  ( ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) /\ x = y ) -> ( ps <-> x = y ) )
22 16 21 mpbird 
 |-  ( ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) /\ x = y ) -> ps )
23 trud 
 |-  ( ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) /\ x = y ) -> T. )
24 22 23 2thd 
 |-  ( ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) /\ x = y ) -> ( ps <-> T. ) )
25 12 13 14 15 24 riota2df 
 |-  ( ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) /\ E! x e. A ps ) -> ( T. <-> ( iota_ x e. A ps ) = y ) )
26 7 25 mpdan 
 |-  ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) -> ( T. <-> ( iota_ x e. A ps ) = y ) )
27 5 26 mpbid 
 |-  ( ( ph /\ ( y e. A /\ A. x e. A ( ps <-> x = y ) ) ) -> ( iota_ x e. A ps ) = y )
28 27 expr 
 |-  ( ( ph /\ y e. A ) -> ( A. x e. A ( ps <-> x = y ) -> ( iota_ x e. A ps ) = y ) )
29 28 ralrimiva 
 |-  ( ph -> A. y e. A ( A. x e. A ( ps <-> x = y ) -> ( iota_ x e. A ps ) = y ) )
30 rspsbc 
 |-  ( B e. A -> ( A. y e. A ( A. x e. A ( ps <-> x = y ) -> ( iota_ x e. A ps ) = y ) -> [. B / y ]. ( A. x e. A ( ps <-> x = y ) -> ( iota_ x e. A ps ) = y ) ) )
31 2 29 30 sylc 
 |-  ( ph -> [. B / y ]. ( A. x e. A ( ps <-> x = y ) -> ( iota_ x e. A ps ) = y ) )
32 nfcvd 
 |-  ( ph -> F/_ x y )
33 32 1 nfeqd 
 |-  ( ph -> F/ x y = B )
34 8 33 nfan1 
 |-  F/ x ( ph /\ y = B )
35 simpr 
 |-  ( ( ph /\ y = B ) -> y = B )
36 35 eqeq2d 
 |-  ( ( ph /\ y = B ) -> ( x = y <-> x = B ) )
37 36 bibi2d 
 |-  ( ( ph /\ y = B ) -> ( ( ps <-> x = y ) <-> ( ps <-> x = B ) ) )
38 34 37 ralbid 
 |-  ( ( ph /\ y = B ) -> ( A. x e. A ( ps <-> x = y ) <-> A. x e. A ( ps <-> x = B ) ) )
39 35 eqeq2d 
 |-  ( ( ph /\ y = B ) -> ( ( iota_ x e. A ps ) = y <-> ( iota_ x e. A ps ) = B ) )
40 38 39 imbi12d 
 |-  ( ( ph /\ y = B ) -> ( ( A. x e. A ( ps <-> x = y ) -> ( iota_ x e. A ps ) = y ) <-> ( A. x e. A ( ps <-> x = B ) -> ( iota_ x e. A ps ) = B ) ) )
41 2 40 sbcied 
 |-  ( ph -> ( [. B / y ]. ( A. x e. A ( ps <-> x = y ) -> ( iota_ x e. A ps ) = y ) <-> ( A. x e. A ( ps <-> x = B ) -> ( iota_ x e. A ps ) = B ) ) )
42 31 41 mpbid 
 |-  ( ph -> ( A. x e. A ( ps <-> x = B ) -> ( iota_ x e. A ps ) = B ) )
43 4 42 mpd 
 |-  ( ph -> ( iota_ x e. A ps ) = B )