Theorem csbex 5235

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

Step	Hyp	Ref	Expression
1		csbexg 5234	. 2 ⊢ (∀𝑥 𝐵 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 ∈ V)
2		csbex.1	. 2 ⊢ 𝐵 ∈ V
3	1, 2	mpg 1800	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3432  ⦋csb 3832

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-nul 5230

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-nul 4257

This theorem is referenced by:  iunopeqop  5435  dfmpo  7942  cantnfdm  9422  cantnff  9432  bpolylem  15758  ruclem1  15940  pcmpt  16593  cidffn  17387  issubc  17550  natffn  17665  fnxpc  17893  evlfcl  17940  odf  19145  selvval  21328  itgfsum  24991  itgparts  25211  vmaf  26268  ttgval  27236  ttgvalOLD  27237  abfmpel  30992  msrf  33504  rdgssun  35549  finxpreclem2  35561  poimirlem17  35794  poimirlem23  35800  poimirlem24  35801  unirep  35871  cdlemk40  38931  aomclem6  40884  rnghmfn  45448  rngchomrnghmresALTV  45554