Theorem csbex 5268

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450  ⦋csb 3864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-nul 5263

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-nul 4299

This theorem is referenced by:  iunopeqop  5483  dfmpo  8083  cantnfdm  9623  cantnff  9633  bpolylem  16020  ruclem1  16205  pcmpt  16869  cidffn  17645  issubc  17803  natffn  17920  fnxpc  18143  evlfcl  18189  odf  19473  rnghmfn  20354  selvval  22028  itgfsum  25734  itgparts  25960  vmaf  27035  mulsval  28018  precsexlem3  28117  ttgval  28808  abfmpel  32585  msrf  35529  rdgssun  37361  finxpreclem2  37373  poimirlem17  37626  poimirlem23  37632  poimirlem24  37633  unirep  37703  cdlemk40  40906  aomclem6  43041  rngchomrnghmresALTV  48257  idfurcl  49077  fucofn2  49303  dfinito4  49480  dftermo4  49481  lanfn  49588  ranfn  49589