Theorem csbex 5257

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

Syntax hints:   ∈ wcel 2114  Vcvv 3441  ⦋csb 3850

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 5252

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 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-nul 4287

This theorem is referenced by:  iunopeqop  5470  dfmpo  8047  cantnfdm  9578  cantnff  9588  bpolylem  15976  ruclem1  16161  pcmpt  16825  cidffn  17606  issubc  17764  natffn  17881  fnxpc  18104  evlfcl  18150  odf  19471  rnghmfn  20380  selvval  22083  itgfsum  25789  itgparts  26015  vmaf  27090  mulsval  28110  precsexlem3  28210  ttgval  28952  abfmpel  32737  msrf  35749  rdgssun  37596  finxpreclem2  37608  poimirlem17  37851  poimirlem23  37857  poimirlem24  37858  unirep  37928  cdlemk40  41256  aomclem6  43379  rngchomrnghmresALTV  48602  idfurcl  49420  fucofn2  49646  dfinito4  49823  dftermo4  49824  lanfn  49931  ranfn  49932