Theorem csbex 5176

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

Syntax hints:   ∈ wcel 2113  Vcvv 3397  ⦋csb 3788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-nul 5171

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-nul 4210

This theorem is referenced by:  iunopeqop  5375  dfmpo  7816  cantnfdm  9193  cantnff  9203  bpolylem  15487  ruclem1  15669  pcmpt  16321  cidffn  17045  issubc  17203  natffn  17317  fnxpc  17535  evlfcl  17581  odf  18776  selvval  20925  itgfsum  24571  itgparts  24791  vmaf  25848  ttgval  26813  abfmpel  30559  msrf  33067  rdgssun  35161  finxpreclem2  35173  poimirlem17  35406  poimirlem23  35412  poimirlem24  35413  unirep  35483  cdlemk40  38543  aomclem6  40440  rnghmfn  44966  rngchomrnghmresALTV  45072