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

Theorem diffi 7786
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 3570 . 2  |-  ( A 
\  B )  C_  A
2 ssfi 7775 . 2  |-  ( ( A  e.  Fin  /\  ( A  \  B ) 
C_  A )  -> 
( A  \  B
)  e.  Fin )
31, 2mpan2 669 1  |-  ( A  e.  Fin  ->  ( A  \  B )  e. 
Fin )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842    \ cdif 3411    C_ wss 3414   Fincfn 7554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-sbc 3278  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-om 6684  df-er 7348  df-en 7555  df-fin 7558
This theorem is referenced by:  dif1en  7787  unfi  7821  dif1card  8420  hashun2  12499  hashun3  12500  hashssdif  12524  hashfun  12544  hashf1lem2  12554  incexc  13800  ramub1lem1  14753  ramub1lem2  14754  psgnprfval  16870  sylow2alem2  16962  sylow2a  16963  gsummgp0  17576  psgnfix1  18932  psgndiflemB  18934  psgndif  18936  zrhcopsgndif  18937  dmatmul  19291  submaval  19375  1marepvsma1  19377  gsummatr01lem3  19451  gsummatr01  19453  smadiadetlem3  19462  smadiadet  19464  cramerimplem1  19477  cmpcld  20195  alexsubALTlem3  20841  cldsubg  20901  xrge0gsumle  21630  amgm  23646  rpvmasum2  24078  cusgrafilem3  24898  frghash2spot  25480  usgreghash2spotv  25483  gsummptres  28227  gsumesum  28506  ballotlemfp1  28936  ballotlemgun  28969  subfacp1lem1  29476  subfacp1lem3  29479  topdifinfindis  31263  elrfi  34988  eldioph2lem1  35054  eldioph2lem2  35055  pellexlem5  35130  fsumnncl  36940  fsumsplit1  36941  fprodeq0g  36969  fprod0  36971  dvmptfprodlem  37109  stoweidlem44  37194  stoweidlem57  37207  fourierdlem42  37299  fourierdlem102  37359  fourierdlem114  37371  etransclem25  37410  etransclem35  37420  fsummsndifre  37974  fsummmodsndifre  37976  mgpsumunsn  38462  mgpsumz  38463  mgpsumn  38464
  Copyright terms: Public domain W3C validator