Theorem csbex 5262

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ⦋csb 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-nul 5257

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-nul 4287

This theorem is referenced by:  iunopeqop  5491  iunopeqopOLD  5492  dfmpo  8081  cantnfdm  9617  cantnff  9627  bpolylem  16088  ruclem1  16273  pcmpt  16938  cidffn  17720  issubc  17878  natffn  17995  fnxpc  18218  evlfcl  18264  odf  19587  rnghmfn  20498  selvval  22180  itgfsum  25896  itgparts  26116  vmaf  27190  mulsval  28209  precsexlem3  28309  ttgval  29082  abfmpel  32863  msrf  35897  rdgssun  37877  finxpreclem2  37889  poimirlem17  38141  poimirlem23  38147  poimirlem24  38148  unirep  38218  cdlemk40  41546  aomclem6  43641  rngchomrnghmresALTV  48892  idfurcl  49710  fucofn2  49936  dfinito4  50113  dftermo4  50114  lanfn  50221  ranfn  50222