Theorem csbex 5247

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ⦋csb 3838

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-nul 4275

This theorem is referenced by:  iunopeqop  5476  dfmpo  8052  cantnfdm  9585  cantnff  9595  bpolylem  16013  ruclem1  16198  pcmpt  16863  cidffn  17644  issubc  17802  natffn  17919  fnxpc  18142  evlfcl  18188  odf  19512  rnghmfn  20419  selvval  22101  itgfsum  25794  itgparts  26014  vmaf  27082  mulsval  28101  precsexlem3  28201  ttgval  28943  abfmpel  32728  msrf  35724  rdgssun  37694  finxpreclem2  37706  poimirlem17  37958  poimirlem23  37964  poimirlem24  37965  unirep  38035  cdlemk40  41363  aomclem6  43487  rngchomrnghmresALTV  48749  idfurcl  49567  fucofn2  49793  dfinito4  49970  dftermo4  49971  lanfn  50078  ranfn  50079