Theorem csbex 5266

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  ⦋csb 3862

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 2701  ax-nul 5261

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 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-nul 4297

This theorem is referenced by:  iunopeqop  5481  dfmpo  8081  cantnfdm  9617  cantnff  9627  bpolylem  16014  ruclem1  16199  pcmpt  16863  cidffn  17639  issubc  17797  natffn  17914  fnxpc  18137  evlfcl  18183  odf  19467  rnghmfn  20348  selvval  22022  itgfsum  25728  itgparts  25954  vmaf  27029  mulsval  28012  precsexlem3  28111  ttgval  28802  abfmpel  32579  msrf  35529  rdgssun  37366  finxpreclem2  37378  poimirlem17  37631  poimirlem23  37637  poimirlem24  37638  unirep  37708  cdlemk40  40911  aomclem6  43048  rngchomrnghmresALTV  48267  idfurcl  49087  fucofn2  49313  dfinito4  49490  dftermo4  49491  lanfn  49598  ranfn  49599