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.

Step	Hyp	Ref	Expression
1		df-fin 7540	. . 3
2	1	eleq2i 2535	. 2
3		relen 7541	. . . . 5
4	3	brrelexi 5045	. . . 4
5	4	rexlimivw 2946	. . 3
6		breq1 4455	. . . 4
7	6	rexbidv 2968	. . 3
8	5, 7	elab3 3253	. 2
9	2, 8	bitri 249	1

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