Theorem csbex 5273

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

This proof depends on syntax axioms:   ∈ wcel 2142  Vcvv 3454  ⦋csb 3852

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-nul 5268

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-nul 4286

This theorem is used by:  iunopeqop  5503  iunopeqopOLD  5504  dfmpo  8095  cantnfdm  9631  cantnff  9641  bpolylem  16108  ruclem1  16293  pcmpt  16958  cidffn  17740  issubc  17898  natffn  18015  fnxpc  18238  evlfcl  18284  odf  19613  rnghmfn  20528  selvval  22282  itgfsum  25997  itgparts  26217  vmaf  27294  mulsval  28313  precsexlem3  28413  ttgval  29235  abfmpel  33011  msrf  36042  rdgssun  38052  finxpreclem2  38064  poimirlem17  38316  poimirlem23  38322  poimirlem24  38323  unirep  38393  cdlemk40  41719  aomclem6  43814  rngchomrnghmresALTV  49072  idfurcl  49904  fucofn2  50130  dfinito4  50307  dftermo4  50308  lanfn  50415  ranfn  50416