Theorem csbex 5311

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 5310	. 2 ⊢ (∀𝑥 𝐵 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 ∈ V)
2		csbex.1	. 2 ⊢ 𝐵 ∈ V
3	1, 2	mpg 1799	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3474  ⦋csb 3893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2703  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-nul 4323

This theorem is referenced by:  iunopeqop  5521  dfmpo  8087  cantnfdm  9658  cantnff  9668  bpolylem  15991  ruclem1  16173  pcmpt  16824  cidffn  17621  issubc  17784  natffn  17899  fnxpc  18127  evlfcl  18174  odf  19404  selvval  21680  itgfsum  25343  itgparts  25563  vmaf  26620  mulsval  27562  precsexlem3  27652  ttgval  28123  ttgvalOLD  28124  abfmpel  31875  msrf  34528  rdgssun  36254  finxpreclem2  36266  poimirlem17  36500  poimirlem23  36506  poimirlem24  36507  unirep  36577  cdlemk40  39783  aomclem6  41791  rnghmfn  46678  rngchomrnghmresALTV  46884