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

Theorem csbex 5212
 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 𝐵 ∈ V
Assertion
Ref Expression
csbex 𝐴 / 𝑥𝐵 ∈ V

Proof of Theorem csbex
StepHypRef Expression
1 csbexg 5211 . 2 (∀𝑥 𝐵 ∈ V → 𝐴 / 𝑥𝐵 ∈ V)
2 csbex.1 . 2 𝐵 ∈ V
31, 2mpg 1791 1 𝐴 / 𝑥𝐵 ∈ V
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2107  Vcvv 3500  ⦋csb 3887 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-nul 5207 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-nul 4296 This theorem is referenced by:  iunopeqop  5408  dfmpo  7793  cantnfdm  9121  cantnff  9131  bpolylem  15397  ruclem1  15579  pcmpt  16223  cidffn  16944  issubc  17100  natffn  17214  fnxpc  17421  evlfcl  17467  odf  18601  selvval  20266  itgfsum  24361  itgparts  24578  vmaf  25629  ttgval  26594  abfmpel  30334  msrf  32692  rdgssun  34547  finxpreclem2  34559  poimirlem17  34795  poimirlem23  34801  poimirlem24  34802  unirep  34875  cdlemk40  37939  aomclem6  39543  rnghmfn  44063  rngchomrnghmresALTV  44169
 Copyright terms: Public domain W3C validator