# Metamath Proof Explorer

## Theorem csbiebt

Description: Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf .) (Contributed by NM, 11-Nov-2005)

Ref Expression
Assertion csbiebt

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{A}\in {V}\to {A}\in \mathrm{V}$
2 spsbc
4 simpl ${⊢}\left({A}\in \mathrm{V}\wedge \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}\right)\to {A}\in \mathrm{V}$
5 biimt ${⊢}{x}={A}\to \left({B}={C}↔\left({x}={A}\to {B}={C}\right)\right)$
6 csbeq1a
7 6 eqeq1d
8 5 7 bitr3d
10 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{V}$
11 nfnfc1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
12 10 11 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{V}\wedge \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}\right)$
13 nfcsb1v
14 13 a1i
15 simpr ${⊢}\left({A}\in \mathrm{V}\wedge \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}\right)\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
16 14 15 nfeqd
17 4 9 12 16 sbciedf
18 3 17 sylibd
19 13 a1i
20 id ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
21 19 20 nfeqd
22 11 21 nfan1
23 7 biimprcd