Theorem csbex 4793

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

Syntax hints:   ∈ wcel 1990  Vcvv 3200  ⦋csb 3533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-nul 3916

This theorem is referenced by:  iunopeqop  4981  dfmpt2  7267  cantnfdm  8561  cantnff  8571  bpolylem  14779  ruclem1  14960  pcmpt  15596  cidffn  16339  issubc  16495  natffn  16609  fnxpc  16816  evlfcl  16862  odf  17956  itgfsum  23593  itgparts  23810  vmaf  24845  ttgval  25755  abfmpel  29455  msrf  31439  finxpreclem2  33227  poimirlem17  33426  poimirlem23  33432  poimirlem24  33433  unirep  33507  cdlemk40  36205  aomclem6  37629  rnghmfn  41890  rngchomrnghmresALTV  41996