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

Theorem f1eq1 5762
Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1eq1  |-  ( F  =  G  ->  ( F : A -1-1-> B  <->  G : A -1-1-> B ) )

Proof of Theorem f1eq1
StepHypRef Expression
1 feq1 5699 . . 3  |-  ( F  =  G  ->  ( F : A --> B  <->  G : A
--> B ) )
2 cnveq 5162 . . . 4  |-  ( F  =  G  ->  `' F  =  `' G
)
32funeqd 5595 . . 3  |-  ( F  =  G  ->  ( Fun  `' F  <->  Fun  `' G ) )
41, 3anbi12d 710 . 2  |-  ( F  =  G  ->  (
( F : A --> B  /\  Fun  `' F
)  <->  ( G : A
--> B  /\  Fun  `' G ) ) )
5 df-f1 5579 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
6 df-f1 5579 . 2  |-  ( G : A -1-1-> B  <->  ( G : A --> B  /\  Fun  `' G ) )
74, 5, 63bitr4g 288 1  |-  ( F  =  G  ->  ( F : A -1-1-> B  <->  G : A -1-1-> B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1381   `'ccnv 4984   Fun wfun 5568   -->wf 5570   -1-1->wf1 5571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-br 4434  df-opab 4492  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579
This theorem is referenced by:  f1oeq1  5793  f1eq123d  5797  fo00  5835  fun11iun  6741  tposf12  6978  oacomf1olem  7211  f1dom2g  7531  f1domg  7533  dom3d  7555  domtr  7566  domssex2  7675  1sdom  7720  marypha1lem  7891  fseqenlem1  8403  dfac12lem2  8522  dfac12lem3  8523  ackbij2  8621  fin23lem28  8718  fin23lem32  8722  fin23lem34  8724  fin23lem35  8725  fin23lem41  8730  iundom2g  8913  pwfseqlem5  9039  hashf1lem1  12478  hashf1lem2  12479  hashf1  12480  4sqlem11  14345  conjsubgen  16168  sylow1lem2  16488  sylow2blem1  16509  hauspwpwf1  20354  istrkg2ld  23723  axlowdim  24129  isuslgra  24208  isusgra  24209  usgrares  24234  sizeusglecusg  24351  2trllemE  24420  constr1trl  24455  specval  26682  zrhchr  27823  qqhre  27864  eldioph2lem2  30662
  Copyright terms: Public domain W3C validator