Theorem csbex 5264

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 4047  df-nul 4279

This theorem is used by:  iunopeqop  5493  iunopeqopOLD  5494  dfmpo  8113  cantnfdm  9665  cantnff  9675  bpolylem  16214  ruclem1  16399  pcmpt  17070  cidffn  17852  issubc  18010  natffn  18127  fnxpc  18350  evlfcl  18396  odf  19751  rnghmfn  20669  selvval  22429  itgfsum  26147  itgparts  26367  vmaf  27446  mulsval  28495  precsexlem3  28595  ttgval  29452  abfmpel  33291  msrf  36349  rdgssun  38344  finxpreclem2  38356  poimirlem17  38598  poimirlem23  38604  poimirlem24  38605  unirep  38691  cdlemk40  42017  aomclem6  44104  rngchomrnghmresALTV  49419  idfurcl  50249  fucofn2  50475  dfinito4  50652  dftermo4  50653  lanfn  50760  ranfn  50761