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

Metamath Proof Explorer

Theorem csbexg

Description: The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005) (Revised by NM, 17-Aug-2018)

Ref Expression
Assertion csbexg 
|- ( A. x B e. W -> [_ A / x ]_ B e. _V )

Proof

Step Hyp Ref Expression
1 df-csb 
 |-  [_ A / x ]_ B = { y | [. A / x ]. y e. B }
2 abid2 
 |-  { y | y e. B } = B
3 elex 
 |-  ( B e. W -> B e. _V )
4 2 3 eqeltrid 
 |-  ( B e. W -> { y | y e. B } e. _V )
5 4 alimi 
 |-  ( A. x B e. W -> A. x { y | y e. B } e. _V )
6 spsbc 
 |-  ( A e. _V -> ( A. x { y | y e. B } e. _V -> [. A / x ]. { y | y e. B } e. _V ) )
7 5 6 syl5 
 |-  ( A e. _V -> ( A. x B e. W -> [. A / x ]. { y | y e. B } e. _V ) )
8 nfcv 
 |-  F/_ x _V
9 8 sbcabel 
 |-  ( A e. _V -> ( [. A / x ]. { y | y e. B } e. _V <-> { y | [. A / x ]. y e. B } e. _V ) )
10 7 9 sylibd 
 |-  ( A e. _V -> ( A. x B e. W -> { y | [. A / x ]. y e. B } e. _V ) )
11 10 imp 
 |-  ( ( A e. _V /\ A. x B e. W ) -> { y | [. A / x ]. y e. B } e. _V )
12 1 11 eqeltrid 
 |-  ( ( A e. _V /\ A. x B e. W ) -> [_ A / x ]_ B e. _V )
13 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ B = (/) )
14 0ex 
 |-  (/) e. _V
15 13 14 eqeltrdi 
 |-  ( -. A e. _V -> [_ A / x ]_ B e. _V )
16 15 adantr 
 |-  ( ( -. A e. _V /\ A. x B e. W ) -> [_ A / x ]_ B e. _V )
17 12 16 pm2.61ian 
 |-  ( A. x B e. W -> [_ A / x ]_ B e. _V )