Theorem difexg 5233

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 4110	. 2 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
2		ssexg 5229	. 2 ⊢ (((𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (𝐴 ∖ 𝐵) ∈ V)
3	1, 2	mpan 688	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3496   ∖ cdif 3935   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-in 3945  df-ss 3954

This theorem is referenced by:  difexi  5234  difex2  7484  elpwun  7493  2oconcl  8130  fnoe  8137  ralxpmap  8462  difsnen  8601  domdifsn  8602  domunsncan  8619  fodomr  8670  domss2  8678  domssex2  8679  domssex  8680  mapdom2  8690  limenpsi  8694  sucdom2  8716  brwdom2  9039  infeq5i  9101  infdifsn  9122  dfac8clem  9460  acni  9473  infdif  9633  infpss  9641  ssfin4  9734  isf34lem1  9796  compssiso  9798  enfin1ai  9808  fin1a2lem7  9830  fin1a2lem13  9836  fpwwe2lem13  10066  fpwwe2  10067  canthp1lem1  10076  hashgt23el  13788  hashf1lem1  13816  brfi1indALT  13861  mrieqv2d  16912  mreexexlemd  16917  pmtrfv  18582  dpjidcl  19182  isirred  19451  isdrng2  19514  drngmcl  19517  drngid2  19520  isdrngd  19529  subdrgint  19584  cnmsubglem  20610  islindf4  20984  smadiadetlem1a  21274  basdif0  21563  tgdif0  21602  clsval2  21660  pnrmopn  21953  cmpcld  22012  cmpfi  22018  csdfil  22504  ufileu  22529  filufint  22530  alexsublem  22654  ptcmplem2  22663  bcth3  23936  iunmbl  24156  tdeglem4  24656  logbfval  25370  nbfusgrlevtxm2  27162  vtxdginducedm1  27327  frgrwopreglem1  28093  eigvecval  29675  elpwdifcl  30289  disjdifprg  30327  padct  30457  resf1o  30468  xrge00  30675  xrge0tsmsd  30694  tocycfv  30753  tocycf  30761  cyc3conja  30801  locfinref  31107  esummono  31315  esumpad  31316  esumpad2  31317  insiga  31398  ldsysgenld  31421  sigapildsys  31423  carsgclctun  31581  sitgclg  31602  ballotlemfrc  31786  ballotlem8  31796  bnj852  32195  bnj865  32197  subfacp1lem5  32433  iscvm  32508  cvmsval  32515  mdvval  32753  topdifinffinlem  34630  pibt2  34700  poimirlem15  34909  voliunnfl  34938  fdc  35022  isdrngo2  35238  selvval2lemn  39142  selvval2lem4  39143  selvval2lem5  39144  selvcl  39145  lzenom  39374  diophin  39376  diophren  39417  deg1mhm  39814  clcnvlem  39990  dssmapfv3d  40372  dssmapnvod  40373  ovolsplit  42280  stoweidlem57  42349  fourierdlem102  42500  fourierdlem114  42512  pwsal  42607  intsal  42620  gsumge0cl  42660  sge0ss  42701  sge0fodjrnlem  42705  iundjiunlem  42748  iundjiun  42749  meaiunlelem  42757  caragendifcl  42803  carageniuncllem1  42810  isomenndlem  42819  hoidmv1lelem2  42881  lincdifsn  44486  lindslinindsimp1  44519  lindslinindimp2lem2  44521  lindslinindimp2lem4  44523  lindslinindsimp2lem5  44524  lindslinindsimp2  44525  lincresunit1  44539  lincresunit2  44540  lincresunit3lem2  44542  lincresunit3  44543