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

Syntax hints:   ∈ wcel 2110  Vcvv 3434  ⦋csb 3848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-nul 4282

This theorem is referenced by:  iunopeqop  5459  dfmpo  8027  cantnfdm  9549  cantnff  9559  bpolylem  15947  ruclem1  16132  pcmpt  16796  cidffn  17576  issubc  17734  natffn  17851  fnxpc  18074  evlfcl  18120  odf  19442  rnghmfn  20350  selvval  22043  itgfsum  25748  itgparts  25974  vmaf  27049  mulsval  28041  precsexlem3  28140  ttgval  28846  abfmpel  32627  msrf  35554  rdgssun  37391  finxpreclem2  37403  poimirlem17  37656  poimirlem23  37662  poimirlem24  37663  unirep  37733  cdlemk40  40935  aomclem6  43071  rngchomrnghmresALTV  48289  idfurcl  49109  fucofn2  49335  dfinito4  49512  dftermo4  49513  lanfn  49620  ranfn  49621