Theorem csbex 5246

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-nul 4275

This theorem is referenced by:  iunopeqop  5467  dfmpo  8043  cantnfdm  9574  cantnff  9584  bpolylem  15972  ruclem1  16157  pcmpt  16821  cidffn  17602  issubc  17760  natffn  17877  fnxpc  18100  evlfcl  18146  odf  19470  rnghmfn  20377  selvval  22079  itgfsum  25772  itgparts  25995  vmaf  27069  mulsval  28089  precsexlem3  28189  ttgval  28931  abfmpel  32717  msrf  35730  rdgssun  37690  finxpreclem2  37702  poimirlem17  37949  poimirlem23  37955  poimirlem24  37956  unirep  38026  cdlemk40  41354  aomclem6  43490  rngchomrnghmresALTV  48713  idfurcl  49531  fucofn2  49757  dfinito4  49934  dftermo4  49935  lanfn  50042  ranfn  50043