Theorem csbex 5251

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ⦋csb 3845

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-nul 5246

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 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-nul 4283

This theorem is referenced by:  iunopeqop  5464  dfmpo  8038  cantnfdm  9560  cantnff  9570  bpolylem  15961  ruclem1  16146  pcmpt  16810  cidffn  17590  issubc  17748  natffn  17865  fnxpc  18088  evlfcl  18134  odf  19455  rnghmfn  20363  selvval  22056  itgfsum  25761  itgparts  25987  vmaf  27062  mulsval  28054  precsexlem3  28153  ttgval  28859  abfmpel  32644  msrf  35593  rdgssun  37429  finxpreclem2  37441  poimirlem17  37683  poimirlem23  37689  poimirlem24  37690  unirep  37760  cdlemk40  41022  aomclem6  43157  rngchomrnghmresALTV  48384  idfurcl  49204  fucofn2  49430  dfinito4  49607  dftermo4  49608  lanfn  49715  ranfn  49716