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

Theorem csbex 5272
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 5271 . 2 (∀𝑥 𝐵 ∈ V → 𝐴 / 𝑥𝐵 ∈ V)
2 csbex.1 . 2 𝐵 ∈ V
31, 2mpg 1800 1 𝐴 / 𝑥𝐵 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3447  csb 3859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-nul 5267
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-nul 4287
This theorem is referenced by:  iunopeqop  5482  dfmpo  8038  cantnfdm  9608  cantnff  9618  bpolylem  15939  ruclem1  16121  pcmpt  16772  cidffn  17566  issubc  17729  natffn  17844  fnxpc  18072  evlfcl  18119  odf  19327  selvval  21551  itgfsum  25214  itgparts  25434  vmaf  26491  mulsval  27403  ttgval  27866  ttgvalOLD  27867  abfmpel  31624  msrf  34200  rdgssun  35899  finxpreclem2  35911  poimirlem17  36145  poimirlem23  36151  poimirlem24  36152  unirep  36222  cdlemk40  39430  aomclem6  41433  rnghmfn  46278  rngchomrnghmresALTV  46384
  Copyright terms: Public domain W3C validator