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

Theorem csbex 3205
Description: The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Hypotheses
Ref Expression
csbex.1  |-  A  e. 
_V
csbex.2  |-  B  e. 
_V
Assertion
Ref Expression
csbex  |-  [_ A  /  x ]_ B  e. 
_V

Proof of Theorem csbex
StepHypRef Expression
1 csbex.1 . . 3  |-  A  e. 
_V
2 csbexg 3204 . . 3  |-  ( ( A  e.  _V  /\  A. x  B  e.  _V )  ->  [_ A  /  x ]_ B  e.  _V )
31, 2mpan 652 . 2  |-  ( A. x  B  e.  _V  ->  [_ A  /  x ]_ B  e.  _V )
4 csbex.2 . 2  |-  B  e. 
_V
53, 4mpg 1554 1  |-  [_ A  /  x ]_ B  e. 
_V
Colors of variables: wff set class
Syntax hints:   A.wal 1546    e. wcel 1717   _Vcvv 2899   [_csb 3194
This theorem is referenced by:  dfmpt2  6376  cantnfdm  7552  cantnff  7562  ruclem1  12757  pcmpt  13188  cidffn  13830  natffn  14073  fnxpc  14200  evlfcl  14246  odf  15102  itgfsum  19585  vmaf  20769  bpolylem  25808  aomclem6  26825
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-sbc 3105  df-csb 3195
  Copyright terms: Public domain W3C validator