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 1830	1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-nul 4279

This theorem is used by:  iunopeqop  5490  iunopeqopOLD  5491  dfmpo  8096  cantnfdm  9643  cantnff  9653  bpolylem  16181  ruclem1  16366  pcmpt  17031  cidffn  17813  issubc  17971  natffn  18088  fnxpc  18311  evlfcl  18357  odf  19712  rnghmfn  20630  selvval  22390  itgfsum  26108  itgparts  26328  vmaf  27409  mulsval  28428  precsexlem3  28528  ttgval  29385  abfmpel  33182  msrf  36228  rdgssun  38221  finxpreclem2  38233  poimirlem17  38475  poimirlem23  38481  poimirlem24  38482  unirep  38568  cdlemk40  41894  aomclem6  44004  rngchomrnghmresALTV  49298  idfurcl  50128  fucofn2  50354  dfinito4  50531  dftermo4  50532  lanfn  50639  ranfn  50640