Theorem csbex 5311

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480  ⦋csb 3899

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-nul 4334

This theorem is referenced by:  iunopeqop  5526  dfmpo  8127  cantnfdm  9704  cantnff  9714  bpolylem  16084  ruclem1  16267  pcmpt  16930  cidffn  17721  issubc  17880  natffn  17997  fnxpc  18221  evlfcl  18267  odf  19555  rnghmfn  20439  selvval  22139  itgfsum  25862  itgparts  26088  vmaf  27162  mulsval  28135  precsexlem3  28233  ttgval  28883  ttgvalOLD  28884  abfmpel  32665  msrf  35547  rdgssun  37379  finxpreclem2  37391  poimirlem17  37644  poimirlem23  37650  poimirlem24  37651  unirep  37721  cdlemk40  40919  aomclem6  43071  rngchomrnghmresALTV  48195  fucofn2  49019