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

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

Proof of Theorem csbex
StepHypRef Expression
1 csbexg 4499 . 2  |-  ( A. x  B  e.  _V  ->  [_ A  /  x ]_ B  e.  _V )
2 csbex.1 . 2  |-  B  e. 
_V
31, 2mpg 1628 1  |-  [_ A  /  x ]_ B  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1826   _Vcvv 3034   [_csb 3348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-nul 4496
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-fal 1405  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-in 3396  df-ss 3403  df-nul 3712
This theorem is referenced by:  dfmpt2  6789  cantnfdm  7994  cantnfdmOLD  7996  cantnff  8006  ruclem1  13966  pcmpt  14413  cidffn  15085  issubc  15241  natffn  15355  fnxpc  15562  evlfcl  15608  odf  16678  itgfsum  22318  itgparts  22533  vmaf  23510  ttgval  24299  abfmpel  27633  msrf  29091  bpolylem  29963  unirep  30369  aomclem6  31171  rnghmfn  32896  rngchomrnghmresALTV  33004  cdlemk40  37056
  Copyright terms: Public domain W3C validator