Theorem difexg 5297

Description: Existence of a difference. (Contributed by NM, 26-May-1998.)

Assertion

Ref	Expression
difexg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)

Proof of Theorem difexg

Step	Hyp	Ref	Expression
1		difss 4098	. 2 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
2		ssexg 5291	. 2 ⊢ (((𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ∖ 𝐵) ∈ V)
3	1, 2	mpan 702	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3463   ∖ cdif 3910   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-in 3920  df-ss 3930

This theorem is referenced by:  difexi  5298  difexd  5299  difex2  7755  elpwun  7764  2oconcl  8484  fnoe  8491  difsnen  9043  fodomr  9112  domss2  9120  domssex2  9121  domssex  9122  limenpsi  9136  dif1enlem  9140  sucdom2  9183  brwdom2  9531  infeq5i  9601  infdifsn  9622  dfac8clem  10012  ssfin4  10290  isf34lem1  10352  compssiso  10354  fin1a2lem7  10386  fin1a2lem13  10392  fpwwe2lem12  10623  hashgt23el  14457  pmtrfv  19518  isirred  20497  isdrng2  20823  drngid2  20831  isdrngd  20843  isdrngdOLD  20845  subdrgint  20880  cnmsubglem  21545  islindf4  21953  smadiadetlem1a  22785  basdif0  23075  tgdif0  23114  clsval2  23172  cmpcld  23524  ptcmplem2  24175  iunmbl  25677  logbfval  26917  nbfusgrlevtxm2  29665  vtxdginducedm1  29830  frgrwopreglem1  30600  eigvecval  32185  elpwdifcl  32809  disjdifprg  32857  mptiffisupp  32975  resf1o  33012  xrge00  33271  xrge0tsmsd  33330  tocycf  33374  ist0cld  34164  locfinref  34172  ldsysgenld  34491  sigapildsys  34493  carsgclctun  34652  sitgclg  34673  ballotlemfrc  34858  ballotlem8  34868  bnj852  35250  bnj865  35252  subfacp1lem5  35571  iscvm  35646  cvmsval  35653  mdvval  35891  ttcwf2  36921  topdifinffinlem  37876  pibt2  37946  poimirlem15  38169  voliunnfl  38198  fdc  38279  isdrngo2  38492  lzenom  43386  diophin  43388  diophren  43425  deg1mhm  43812  stoweidlem57  46656  fourierdlem102  46807  fourierdlem114  46819  pwsal  46914  gsumge0cl  46970  caragendifcl  47113  carageniuncllem1  47120  isomenndlem  47129  hoidmv1lelem2  47191  lincdifsn  49082  lindslinindsimp1  49115  lindslinindimp2lem2  49117  lindslinindimp2lem4  49119  lindslinindsimp2lem5  49120  lindslinindsimp2  49121  lincresunit1  49135  lincresunit2  49136  lincresunit3lem2  49138  lincresunit3  49139