MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difexg Unicode version

Theorem difexg 4162
Description: Existence of a difference. (Contributed by NM, 26-May-1998.)
Assertion
Ref Expression
difexg  |-  ( A  e.  V  ->  ( A  \  B )  e. 
_V )

Proof of Theorem difexg
StepHypRef Expression
1 difss 3303 . 2  |-  ( A 
\  B )  C_  A
2 ssexg 4160 . 2  |-  ( ( ( A  \  B
)  C_  A  /\  A  e.  V )  ->  ( A  \  B
)  e.  _V )
31, 2mpan 651 1  |-  ( A  e.  V  ->  ( A  \  B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   _Vcvv 2788    \ cdif 3149    C_ wss 3152
This theorem is referenced by:  difex2  4525  elpwun  4567  2oconcl  6502  fnoe  6509  difsnen  6944  domdifsn  6945  domunsncan  6962  fodomr  7012  domss2  7020  domssex2  7021  domssex  7022  mapdom2  7032  limenpsi  7036  sucdom2  7057  findcard  7097  findcard2  7098  frfi  7102  unfilem3  7123  marypha1lem  7186  brwdom2  7287  infeq5i  7337  infdifsn  7357  dfac8clem  7659  acni  7672  dfac9  7762  dfacacn  7767  kmlem11  7786  kmlem12  7787  infpss  7843  ssfin4  7936  fin23lem28  7966  isf32lem6  7984  isf32lem7  7985  isf32lem8  7986  isf34lem1  7998  compssiso  8000  enfin1ai  8010  fin1a2lem7  8032  fin1a2lem13  8038  axdc2lem  8074  axcclem  8083  zornn0g  8132  fpwwe2lem13  8264  fpwwe2  8265  canthp1lem1  8274  grothprim  8456  hashbclem  11390  hashf1lem1  11393  ramub1lem1  13073  mrieqv2d  13541  mreexexlemd  13546  pltfval  14093  isirred  15481  isdrng2  15522  drngmcl  15525  drngid2  15528  isdrngd  15537  lssset  15691  xrs1mnd  16409  xrs1cmn  16411  xrge0subm  16412  cnmsubglem  16434  basdif0  16691  tgdif0  16730  clsval2  16787  lecldbas  16949  pnrmopn  17071  cmpcld  17129  cmpfi  17135  csdfil  17589  ufileu  17614  filufint  17615  alexsublem  17738  ptcmplem2  17747  xrge0gsumle  18338  xrge0tsms  18339  bcth3  18753  iunmbl  18910  i1fd  19036  tdeglem4  19446  reefgim  19826  ablomul  21022  eigvecval  22476  ballotlemfrc  23085  ballotlem8  23095  xrge00  23311  disjdifprg  23352  xrge0tsmsd  23382  pwsiga  23491  insiga  23498  subfacp1lem5  23715  iscvm  23790  cvmsval  23797  axlowdimlem15  24584  axlowdim  24589  isdivcv2  25693  isside0  26164  pdiveql  26168  aishp  26172  bhp3  26177  fdc  26455  isdrngo2  26589  ralxpmap  26761  lzenom  26849  diophin  26852  diophren  26896  islindf4  27308  pmtrfv  27395  cntzsdrg  27510  deg1mhm  27526  stoweidlem57  27806  bnj852  28953  bnj865  28955  watvalN  30182  hvmapfval  31949
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator