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

Theorem isfi 7559
 Description: Express " is finite." Definition 10.29 of [TakeutiZaring] p. 91 (whose " " is a predicate instead of a class). (Contributed by NM, 22-Aug-2008.)
Assertion
Ref Expression
isfi
Distinct variable group:   ,

Proof of Theorem isfi
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-fin 7540 . . 3
21eleq2i 2535 . 2
3 relen 7541 . . . . 5
43brrelexi 5045 . . . 4
54rexlimivw 2946 . . 3
6 breq1 4455 . . . 4
76rexbidv 2968 . . 3
85, 7elab3 3253 . 2
92, 8bitri 249 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  =wceq 1395  e.wcel 1818  {cab 2442  E.wrex 2808   cvv 3109   class class class wbr 4452   com 6700   cen 7533   cfn 7536 This theorem is referenced by:  snfi  7616  php3  7723  onfin  7728  fisucdomOLD  7743  ominf  7752  isinf  7753  enfi  7756  ssnnfi  7759  ssfi  7760  dif1enOLD  7772  dif1en  7773  findcard  7779  findcard2  7780  findcard3  7783  nnsdomg  7799  isfiniteg  7800  unfi  7807  fiint  7817  pwfi  7835  finnum  8350  ficardom  8363  dif1card  8409  infpwfien  8464  ficard  8961  hashkf  12407  finminlem  30136 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-rel 5011  df-en 7537  df-fin 7540
 Copyright terms: Public domain W3C validator