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

Theorem feq1 5375
Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
feq1  |-  ( F  =  G  ->  ( F : A --> B  <->  G : A
--> B ) )

Proof of Theorem feq1
StepHypRef Expression
1 fneq1 5333 . . 3  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )
2 rneq 4904 . . . 4  |-  ( F  =  G  ->  ran  F  =  ran  G )
32sseq1d 3205 . . 3  |-  ( F  =  G  ->  ( ran  F  C_  B  <->  ran  G  C_  B ) )
41, 3anbi12d 691 . 2  |-  ( F  =  G  ->  (
( F  Fn  A  /\  ran  F  C_  B
)  <->  ( G  Fn  A  /\  ran  G  C_  B ) ) )
5 df-f 5259 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
6 df-f 5259 . 2  |-  ( G : A --> B  <->  ( G  Fn  A  /\  ran  G  C_  B ) )
74, 5, 63bitr4g 279 1  |-  ( F  =  G  ->  ( F : A --> B  <->  G : A
--> B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    C_ wss 3152   ran crn 4690    Fn wfn 5250   -->wf 5251
This theorem is referenced by:  feq1d  5379  feq1i  5383  elimf  5388  f00  5426  fconstg  5428  f1eq1  5432  fconst2g  5728  fconstfv  5734  elmapg  6785  ac6sfi  7101  ac5num  7663  acni2  7673  cofsmo  7895  cfsmolem  7896  cfcoflem  7898  coftr  7899  alephsing  7902  axdc2lem  8074  axdc3lem2  8077  axdc3lem3  8078  axdc3  8080  axdc4lem  8081  ac6num  8106  inar1  8397  axdc4uzlem  11044  seqf1olem2  11086  seqf1o  11087  iswrd  11415  ramub2  13061  ramcl  13076  isacs2  13555  isacs1i  13559  mreacs  13560  isgrpinv  14532  isghm  14683  1stcfb  17171  upxp  17317  txcn  17320  isi1f  19029  mbfi1fseqlem6  19075  mbfi1flimlem  19077  itg2addlem  19113  plyf  19580  isgrpo  20863  ismgm  20987  elghomlem2  21029  vci  21104  isvclem  21133  isnvlem  21166  ajmoi  21437  ajval  21440  hlimi  21767  chlimi  21814  chcompl  21822  adjmo  22412  adjeu  22469  adjval  22470  adj1  22513  adjeq  22515  cnlnssadj  22660  pjinvari  22771  isrnmeas  23531  iseupa  23881  fprb  24129  orderseqlem  24252  soseq  24254  elno  24300  feq123  25068  fopab2g  25145  mapmapmap  25148  islatalg  25183  domrancur1b  25200  domrancur1c  25202  valcurfn  25203  vecval1b  25451  vecval3b  25452  vri  25492  istopx  25547  ismgra  25710  isalg  25721  algi  25727  filnetlem4  26330  upixp  26403  sdclem2  26452  sdclem1  26453  fdc  26455  ismrc  26776  islindf  27282  fmuldfeqlem1  27712  fmuldfeq  27713  stoweidlem15  27764  stoweidlem16  27765  stoweidlem17  27766  stoweidlem19  27768  stoweidlem20  27769  stoweidlem21  27770  stoweidlem22  27771  stoweidlem23  27772  stoweidlem27  27776  stoweidlem31  27780  stoweidlem32  27781  stoweidlem42  27791  stoweidlem48  27797  stoweidlem51  27800  stoweidlem59  27808  istendo  30949
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-fun 5257  df-fn 5258  df-f 5259
  Copyright terms: Public domain W3C validator