Theorem csbex 5246

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 5245	. 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 5241

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  5467  dfmpo  8043  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  22110  itgfsum  25803  itgparts  26026  vmaf  27100  mulsval  28120  precsexlem3  28220  ttgval  28962  abfmpel  32748  msrf  35745  rdgssun  37705  finxpreclem2  37717  poimirlem17  37969  poimirlem23  37975  poimirlem24  37976  unirep  38046  cdlemk40  41374  aomclem6  43502  rngchomrnghmresALTV  48752  idfurcl  49570  fucofn2  49796  dfinito4  49973  dftermo4  49974  lanfn  50081  ranfn  50082