Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbiebt Structured version   Unicode version

Theorem csbiebt 3450
 Description: Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf 3454.) (Contributed by NM, 11-Nov-2005.)
Assertion
Ref Expression
csbiebt
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem csbiebt
StepHypRef Expression
1 elex 3118 . 2
2 spsbc 3340 . . . . 5
32adantr 465 . . . 4
4 simpl 457 . . . . 5
5 biimt 335 . . . . . . 7
6 csbeq1a 3439 . . . . . . . 8
76eqeq1d 2459 . . . . . . 7
85, 7bitr3d 255 . . . . . 6
98adantl 466 . . . . 5
10 nfv 1708 . . . . . 6
11 nfnfc1 2622 . . . . . 6
1210, 11nfan 1929 . . . . 5
13 nfcsb1v 3446 . . . . . . 7
1413a1i 11 . . . . . 6
15 simpr 461 . . . . . 6
1614, 15nfeqd 2626 . . . . 5
174, 9, 12, 16sbciedf 3363 . . . 4
183, 17sylibd 214 . . 3
1913a1i 11 . . . . . . . 8
20 id 22 . . . . . . . 8
2119, 20nfeqd 2626 . . . . . . 7
2211, 21nfan1 1928 . . . . . 6
237biimprcd 225 . . . . . . 7
2423adantl 466 . . . . . 6
2522, 24alrimi 1878 . . . . 5
2625ex 434 . . . 4