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 1798	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V

Syntax hints:   ∈ wcel 2105  Vcvv 3473  ⦋csb 3893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-nul 4323

This theorem is referenced by:  iunopeqop  5521  dfmpo  8093  cantnfdm  9665  cantnff  9675  bpolylem  15999  ruclem1  16181  pcmpt  16832  cidffn  17629  issubc  17792  natffn  17910  fnxpc  18138  evlfcl  18185  odf  19453  rnghmfn  20337  selvval  21989  itgfsum  25676  itgparts  25902  vmaf  26964  mulsval  27922  precsexlem3  28020  ttgval  28559  ttgvalOLD  28560  abfmpel  32313  msrf  34997  rdgssun  36723  finxpreclem2  36735  poimirlem17  36969  poimirlem23  36975  poimirlem24  36976  unirep  37046  cdlemk40  40252  aomclem6  42264  rngchomrnghmresALTV  47116