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

Theorem csbex 4575
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 4574 . 2  |-  ( A. x  B  e.  _V  ->  [_ A  /  x ]_ B  e.  _V )
2 csbex.1 . 2  |-  B  e. 
_V
31, 2mpg 1598 1  |-  [_ A  /  x ]_ B  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1762   _Vcvv 3108   [_csb 3430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-nul 4571
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-fal 1380  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-v 3110  df-sbc 3327  df-csb 3431  df-dif 3474  df-in 3478  df-ss 3485  df-nul 3781
This theorem is referenced by:  dfmpt2  6865  cantnfdm  8072  cantnfdmOLD  8074  cantnff  8084  ruclem1  13816  pcmpt  14261  cidffn  14924  issubc  15056  natffn  15167  fnxpc  15294  evlfcl  15340  odf  16352  itgfsum  21963  itgparts  22178  vmaf  23116  ttgval  23849  abfmpel  27153  bpolylem  29375  unirep  29795  aomclem6  30600  cdlemk40  35590
  Copyright terms: Public domain W3C validator