Theorem enfi 7814

Description: Equinumerous sets have the same finiteness. (Contributed by NM, 22-Aug-2008.)

Assertion

Ref	Expression
enfi	|- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) )

Proof of Theorem enfi

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		enen1 7738	. . 3 |- ( A ~~ B -> ( A ~~ x <-> B ~~ x ) )
2	1	rexbidv 2913	. 2 |- ( A ~~ B -> ( E. x e. om A ~~ x <-> E. x e. om B ~~ x ) )
3		isfi 7619	. 2 |- ( A e. Fin <-> E. x e. om A ~~ x )
4		isfi 7619	. 2 |- ( B e. Fin <-> E. x e. om B ~~ x )
5	2, 3, 4	3bitr4g 296	1 |- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) )

Syntax hints:   -> wi 4   <-> wb 189   e. wcel 1898   E.wrex 2750   class class class wbr 4416   omcom 6719   ~~ cen 7592   Fincfn 7595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-er 7389  df-en 7596  df-fin 7599

This theorem is referenced by:  enfii  7815  wofib  8086  en2eleq  8465  sdom2en01  8758  fin23lem21  8795  enfin1ai  8840  fin17  8850  isfin7-2  8852  engch  9079  uzinf  12211  hasheni  12563  isfinite4  12575  symggen  17160  psgnunilem1  17183  dfod2  17264  odhash  17272  gsumval3lem1  17588  gsumval3lem2  17589  gsumval3  17590  cyggic  19192  nbusgrafi  25225  cusgrafilem3  25258  eupai  25744  derangen  29944  erdsze2lem1  29975  phpreu  31974  poimirlem30  32015  diophin  35660  diophren  35701  fiphp3d  35707  fiuneneq  36116  cusgrfilem3  39568