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

Theorem diffi 7531
Description: If  A is finite,  ( A  \  B ) is finite. (Contributed by FL, 3-Aug-2009.)
Assertion
Ref Expression
diffi  |-  ( A  e.  Fin  ->  ( A  \  B )  e. 
Fin )

Proof of Theorem diffi
StepHypRef Expression
1 difss 3471 . 2  |-  ( A 
\  B )  C_  A
2 ssfi 7521 . 2  |-  ( ( A  e.  Fin  /\  ( A  \  B ) 
C_  A )  -> 
( A  \  B
)  e.  Fin )
31, 2mpan2 664 1  |-  ( A  e.  Fin  ->  ( A  \  B )  e. 
Fin )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755    \ cdif 3313    C_ wss 3316   Fincfn 7298
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-om 6466  df-er 7089  df-en 7299  df-fin 7302
This theorem is referenced by:  dif1enOLD  7532  dif1en  7533  unfi  7567  dif1card  8165  hashun2  12129  hashun3  12130  hashssdif  12150  hashfun  12182  hashf1lem2  12192  incexc  13282  ramub1lem1  14069  ramub1lem2  14070  psgnran  16000  psgnprfval  16004  sylow2alem2  16096  sylow2a  16097  gsummgp0  16633  psgnfix1  17869  psgndiflemB  17871  psgndif  17873  zrhcopsgndif  17874  submaval  18233  1marepvsma1  18235  gsummatr01lem3  18304  gsummatr01  18306  smadiadetlem3  18315  smadiadet  18317  cramerimplem1  18330  cmpcld  18846  alexsubALTlem3  19462  cldsubg  19522  xrge0gsumle  20251  amgm  22268  rpvmasum2  22645  cusgrafilem3  23211  gsumesum  26363  ballotlemfp1  26721  ballotlemgun  26754  subfacp1lem1  26914  subfacp1lem3  26917  elrfi  28872  eldioph2lem1  28940  eldioph2lem2  28941  pellexlem5  29016  stoweidlem44  29682  stoweidlem57  29695  fsummsndifre  30080  fsummmodsndifre  30082  frghash2spot  30499  usgreghash2spotv  30502  mgpsumunsn  30590  mgpsumz  30591  mgpsumn  30592
  Copyright terms: Public domain W3C validator