Theorem csbex 5272

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453  ⦋csb 3850

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 2215  ax-ext 2734  ax-nul 5267

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 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-nul 4283

This theorem is used by:  iunopeqop  5502  iunopeqopOLD  5503  dfmpo  8102  cantnfdm  9646  cantnff  9656  bpolylem  16138  ruclem1  16323  pcmpt  16988  cidffn  17770  issubc  17928  natffn  18045  fnxpc  18268  evlfcl  18314  odf  19665  rnghmfn  20581  selvval  22337  itgfsum  26056  itgparts  26276  vmaf  27353  mulsval  28372  precsexlem3  28472  ttgval  29317  abfmpel  33115  msrf  36108  rdgssun  38119  finxpreclem2  38131  poimirlem17  38373  poimirlem23  38379  poimirlem24  38380  unirep  38451  cdlemk40  41777  aomclem6  43887  rngchomrnghmresALTV  49181  idfurcl  50011  fucofn2  50237  dfinito4  50414  dftermo4  50415  lanfn  50522  ranfn  50523