Theorem csbex 5329

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ⦋csb 3921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-nul 4353

This theorem is referenced by:  iunopeqop  5540  dfmpo  8143  cantnfdm  9733  cantnff  9743  bpolylem  16096  ruclem1  16279  pcmpt  16939  cidffn  17736  issubc  17899  natffn  18017  fnxpc  18245  evlfcl  18292  odf  19579  rnghmfn  20465  selvval  22162  itgfsum  25882  itgparts  26108  vmaf  27180  mulsval  28153  precsexlem3  28251  ttgval  28901  ttgvalOLD  28902  abfmpel  32673  msrf  35510  rdgssun  37344  finxpreclem2  37356  poimirlem17  37597  poimirlem23  37603  poimirlem24  37604  unirep  37674  cdlemk40  40874  aomclem6  43016  rngchomrnghmresALTV  48002