Theorem csbex 5268

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ⦋csb 3851

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-v 3456  df-sbc 3743  df-csb 3852  df-dif 4050  df-nul 4282

This theorem is used by:  iunopeqop  5498  iunopeqopOLD  5499  dfmpo  8140  cantnfdm  9692  cantnff  9702  bpolylem  16243  ruclem1  16428  pcmpt  17099  cidffn  17881  issubc  18039  natffn  18156  fnxpc  18379  evlfcl  18425  odf  19781  rnghmfn  20699  selvval  22459  itgfsum  26177  itgparts  26397  vmaf  27476  mulsval  28525  precsexlem3  28625  ttgval  29482  abfmpel  33321  msrf  36474  rdgssun  38493  finxpreclem2  38505  poimirlem17  38747  poimirlem23  38753  poimirlem24  38754  unirep  38840  cdlemk40  42166  aomclem6  44254  rngchomrnghmresALTV  49581  idfurcl  50419  fucofn2  50651  dfinito4  50841  dftermo4  50842  lanfn  50997  ranfn  50998