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

Metamath Proof Explorer

Theorem riotasv2s

Description: The value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 ) in the form of a substitution instance. Special case of riota2f . (Contributed by NM, 3-Mar-2013) (Proof shortened by Mario Carneiro, 6-Dec-2016)

Ref Expression
Hypothesis riotasv2s.2 
|- D = ( iota_ x e. A A. y e. B ( ph -> x = C ) )
Assertion riotasv2s 
|- ( ( A e. V /\ D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> D = [_ E / y ]_ C )

Proof

Step Hyp Ref Expression
1 riotasv2s.2 
 |-  D = ( iota_ x e. A A. y e. B ( ph -> x = C ) )
2 3simpc 
 |-  ( ( A e. V /\ D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) )
3 simp1 
 |-  ( ( A e. V /\ D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> A e. V )
4 nfra1 
 |-  F/ y A. y e. B ( ph -> x = C )
5 nfcv 
 |-  F/_ y A
6 4 5 nfriota 
 |-  F/_ y ( iota_ x e. A A. y e. B ( ph -> x = C ) )
7 1 6 nfcxfr 
 |-  F/_ y D
8 7 nfel1 
 |-  F/ y D e. A
9 nfv 
 |-  F/ y E e. B
10 nfsbc1v 
 |-  F/ y [. E / y ]. ph
11 9 10 nfan 
 |-  F/ y ( E e. B /\ [. E / y ]. ph )
12 8 11 nfan 
 |-  F/ y ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) )
13 nfcsb1v 
 |-  F/_ y [_ E / y ]_ C
14 13 a1i 
 |-  ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> F/_ y [_ E / y ]_ C )
15 10 a1i 
 |-  ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> F/ y [. E / y ]. ph )
16 1 a1i 
 |-  ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> D = ( iota_ x e. A A. y e. B ( ph -> x = C ) ) )
17 sbceq1a 
 |-  ( y = E -> ( ph <-> [. E / y ]. ph ) )
18 17 adantl 
 |-  ( ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) /\ y = E ) -> ( ph <-> [. E / y ]. ph ) )
19 csbeq1a 
 |-  ( y = E -> C = [_ E / y ]_ C )
20 19 adantl 
 |-  ( ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) /\ y = E ) -> C = [_ E / y ]_ C )
21 simpl 
 |-  ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> D e. A )
22 simprl 
 |-  ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> E e. B )
23 simprr 
 |-  ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> [. E / y ]. ph )
24 12 14 15 16 18 20 21 22 23 riotasv2d 
 |-  ( ( ( D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) /\ A e. V ) -> D = [_ E / y ]_ C )
25 2 3 24 syl2anc 
 |-  ( ( A e. V /\ D e. A /\ ( E e. B /\ [. E / y ]. ph ) ) -> D = [_ E / y ]_ C )