Theorem csbex 4826

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

Syntax hints:   ∈ wcel 2030  Vcvv 3231  ⦋csb 3566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-nul 3949

This theorem is referenced by:  iunopeqop  5010  dfmpt2  7312  cantnfdm  8599  cantnff  8609  bpolylem  14823  ruclem1  15004  pcmpt  15643  cidffn  16386  issubc  16542  natffn  16656  fnxpc  16863  evlfcl  16909  odf  18002  itgfsum  23638  itgparts  23855  vmaf  24890  ttgval  25800  abfmpel  29583  msrf  31565  finxpreclem2  33357  poimirlem17  33556  poimirlem23  33562  poimirlem24  33563  unirep  33637  cdlemk40  36522  aomclem6  37946  rnghmfn  42215  rngchomrnghmresALTV  42321