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  8046  cantnfdm  9577  cantnff  9587  bpolylem  15975  ruclem1  16160  pcmpt  16824  cidffn  17605  issubc  17763  natffn  17880  fnxpc  18103  evlfcl  18149  odf  19470  rnghmfn  20379  selvval  22082  itgfsum  25788  itgparts  26014  vmaf  27089  mulsval  28091  precsexlem3  28190  ttgval  28930  abfmpel  32715  msrf  35717  rdgssun  37554  finxpreclem2  37566  poimirlem17  37809  poimirlem23  37815  poimirlem24  37816  unirep  37886  cdlemk40  41214  aomclem6  43337  rngchomrnghmresALTV  48561  idfurcl  49379  fucofn2  49605  dfinito4  49782  dftermo4  49783  lanfn  49890  ranfn  49891