# Metamath Proof Explorer

## Theorem csbiota

Description: Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017) (Revised by NM, 23-Aug-2018)

Ref Expression
Assertion csbiota
`|- [_ A / x ]_ ( iota y ph ) = ( iota y [. A / x ]. ph )`

### Proof

Step Hyp Ref Expression
1 csbeq1
` |-  ( z = A -> [_ z / x ]_ ( iota y ph ) = [_ A / x ]_ ( iota y ph ) )`
2 dfsbcq2
` |-  ( z = A -> ( [ z / x ] ph <-> [. A / x ]. ph ) )`
3 2 iotabidv
` |-  ( z = A -> ( iota y [ z / x ] ph ) = ( iota y [. A / x ]. ph ) )`
4 1 3 eqeq12d
` |-  ( z = A -> ( [_ z / x ]_ ( iota y ph ) = ( iota y [ z / x ] ph ) <-> [_ A / x ]_ ( iota y ph ) = ( iota y [. A / x ]. ph ) ) )`
5 vex
` |-  z e. _V`
6 nfs1v
` |-  F/ x [ z / x ] ph`
7 6 nfiotaw
` |-  F/_ x ( iota y [ z / x ] ph )`
8 sbequ12
` |-  ( x = z -> ( ph <-> [ z / x ] ph ) )`
9 8 iotabidv
` |-  ( x = z -> ( iota y ph ) = ( iota y [ z / x ] ph ) )`
10 5 7 9 csbief
` |-  [_ z / x ]_ ( iota y ph ) = ( iota y [ z / x ] ph )`
11 4 10 vtoclg
` |-  ( A e. _V -> [_ A / x ]_ ( iota y ph ) = ( iota y [. A / x ]. ph ) )`
12 csbprc
` |-  ( -. A e. _V -> [_ A / x ]_ ( iota y ph ) = (/) )`
13 sbcex
` |-  ( [. A / x ]. ph -> A e. _V )`
14 13 con3i
` |-  ( -. A e. _V -> -. [. A / x ]. ph )`
15 14 nexdv
` |-  ( -. A e. _V -> -. E. y [. A / x ]. ph )`
16 euex
` |-  ( E! y [. A / x ]. ph -> E. y [. A / x ]. ph )`
17 16 con3i
` |-  ( -. E. y [. A / x ]. ph -> -. E! y [. A / x ]. ph )`
18 iotanul
` |-  ( -. E! y [. A / x ]. ph -> ( iota y [. A / x ]. ph ) = (/) )`
19 15 17 18 3syl
` |-  ( -. A e. _V -> ( iota y [. A / x ]. ph ) = (/) )`
20 12 19 eqtr4d
` |-  ( -. A e. _V -> [_ A / x ]_ ( iota y ph ) = ( iota y [. A / x ]. ph ) )`
21 11 20 pm2.61i
` |-  [_ A / x ]_ ( iota y ph ) = ( iota y [. A / x ]. ph )`