Theorem csbex 5281

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459  ⦋csb 3874

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 2707  ax-nul 5276

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-nul 4309

This theorem is referenced by:  iunopeqop  5496  dfmpo  8101  cantnfdm  9678  cantnff  9688  bpolylem  16064  ruclem1  16249  pcmpt  16912  cidffn  17690  issubc  17848  natffn  17965  fnxpc  18188  evlfcl  18234  odf  19518  rnghmfn  20399  selvval  22073  itgfsum  25780  itgparts  26006  vmaf  27081  mulsval  28064  precsexlem3  28163  ttgval  28854  abfmpel  32633  msrf  35564  rdgssun  37396  finxpreclem2  37408  poimirlem17  37661  poimirlem23  37667  poimirlem24  37668  unirep  37738  cdlemk40  40936  aomclem6  43083  rngchomrnghmresALTV  48254  idfurcl  49058  fucofn2  49235  dfinito4  49386  dftermo4  49387  lanfn  49486  ranfn  49487