Theorem csbex 5230

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422  ⦋csb 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-nul 4254

This theorem is referenced by:  iunopeqop  5429  dfmpo  7913  cantnfdm  9352  cantnff  9362  bpolylem  15686  ruclem1  15868  pcmpt  16521  cidffn  17304  issubc  17466  natffn  17581  fnxpc  17809  evlfcl  17856  odf  19060  selvval  21238  itgfsum  24896  itgparts  25116  vmaf  26173  ttgval  27140  abfmpel  30894  msrf  33404  rdgssun  35476  finxpreclem2  35488  poimirlem17  35721  poimirlem23  35727  poimirlem24  35728  unirep  35798  cdlemk40  38858  aomclem6  40800  rnghmfn  45336  rngchomrnghmresALTV  45442