Theorem csbex 5253

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438  ⦋csb 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-nul 4287

This theorem is referenced by:  iunopeqop  5468  dfmpo  8042  cantnfdm  9579  cantnff  9589  bpolylem  15973  ruclem1  16158  pcmpt  16822  cidffn  17602  issubc  17760  natffn  17877  fnxpc  18100  evlfcl  18146  odf  19434  rnghmfn  20342  selvval  22038  itgfsum  25744  itgparts  25970  vmaf  27045  mulsval  28035  precsexlem3  28134  ttgval  28838  abfmpel  32612  msrf  35514  rdgssun  37351  finxpreclem2  37363  poimirlem17  37616  poimirlem23  37622  poimirlem24  37623  unirep  37693  cdlemk40  40896  aomclem6  43032  rngchomrnghmresALTV  48251  idfurcl  49071  fucofn2  49297  dfinito4  49474  dftermo4  49475  lanfn  49582  ranfn  49583