Theorem csbex 5273

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  ⦋csb 3852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-nul 5268

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-nul 4286

This theorem is referenced by:  iunopeqop  5504  iunopeqopOLD  5505  dfmpo  8096  cantnfdm  9632  cantnff  9642  bpolylem  16101  ruclem1  16286  pcmpt  16951  cidffn  17733  issubc  17891  natffn  18008  fnxpc  18231  evlfcl  18277  odf  19606  rnghmfn  20520  selvval  22250  itgfsum  25965  itgparts  26185  vmaf  27259  mulsval  28278  precsexlem3  28378  ttgval  29190  abfmpel  32966  msrf  35988  rdgssun  37968  finxpreclem2  37980  poimirlem17  38232  poimirlem23  38238  poimirlem24  38239  unirep  38309  cdlemk40  41637  aomclem6  43734  rngchomrnghmresALTV  48989  idfurcl  49821  fucofn2  50047  dfinito4  50224  dftermo4  50225  lanfn  50332  ranfn  50333