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

Theorem f1oen3g 7325
Description: The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 7328 does not require the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.)
Assertion
Ref Expression
f1oen3g  |-  ( ( F  e.  V  /\  F : A -1-1-onto-> B )  ->  A  ~~  B )

Proof of Theorem f1oen3g
Dummy variable  f is distinct from all other variables.
StepHypRef Expression
1 f1oeq1 5632 . . . 4  |-  ( f  =  F  ->  (
f : A -1-1-onto-> B  <->  F : A
-1-1-onto-> B ) )
21spcegv 3058 . . 3  |-  ( F  e.  V  ->  ( F : A -1-1-onto-> B  ->  E. f 
f : A -1-1-onto-> B ) )
32imp 429 . 2  |-  ( ( F  e.  V  /\  F : A -1-1-onto-> B )  ->  E. f 
f : A -1-1-onto-> B )
4 bren 7319 . 2  |-  ( A 
~~  B  <->  E. f 
f : A -1-1-onto-> B )
53, 4sylibr 212 1  |-  ( ( F  e.  V  /\  F : A -1-1-onto-> B )  ->  A  ~~  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1586    e. wcel 1756   class class class wbr 4292   -1-1-onto->wf1o 5417    ~~ cen 7307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531  ax-un 6372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-en 7311
This theorem is referenced by:  f1oen2g  7326  unen  7392  domdifsn  7394  domunsncan  7411  sbthlem10  7430  domssex  7472  phplem2  7491  sucdom2  7507  pssnn  7531  f1finf1o  7539  oien  7752  infdifsn  7862  fin4en1  8478  fin23lem21  8508  hashf1lem2  12209  odinf  16064  gsumval3OLD  16382  gsumval3lem1  16383  gsumval3lem2  16384  gsumval3  16385  hmphen2  19372
  Copyright terms: Public domain W3C validator