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 1799	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3427  ⦋csb 3833

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 2184  ax-ext 2707  ax-nul 5230

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 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-nul 4264

This theorem is referenced by:  iunopeqop  5464  iunopeqopOLD  5465  dfmpo  8041  cantnfdm  9574  cantnff  9584  bpolylem  16002  ruclem1  16187  pcmpt  16852  cidffn  17633  issubc  17791  natffn  17908  fnxpc  18131  evlfcl  18177  odf  19501  rnghmfn  20408  selvval  22090  itgfsum  25782  itgparts  26002  vmaf  27070  mulsval  28089  precsexlem3  28189  ttgval  28931  abfmpel  32716  msrf  35712  rdgssun  37682  finxpreclem2  37694  poimirlem17  37946  poimirlem23  37952  poimirlem24  37953  unirep  38023  cdlemk40  41351  aomclem6  43475  rngchomrnghmresALTV  48743  idfurcl  49561  fucofn2  49787  dfinito4  49964  dftermo4  49965  lanfn  50072  ranfn  50073