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

Theorem feq1 5516
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 5474 . . 3  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )
2 rneq 5035 . . . 4  |-  ( F  =  G  ->  ran  F  =  ran  G )
32sseq1d 3318 . . 3  |-  ( F  =  G  ->  ( ran  F  C_  B  <->  ran  G  C_  B ) )
41, 3anbi12d 692 . 2  |-  ( F  =  G  ->  (
( F  Fn  A  /\  ran  F  C_  B
)  <->  ( G  Fn  A  /\  ran  G  C_  B ) ) )
5 df-f 5398 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
6 df-f 5398 . 2  |-  ( G : A --> B  <->  ( G  Fn  A  /\  ran  G  C_  B ) )
74, 5, 63bitr4g 280 1  |-  ( F  =  G  ->  ( F : A --> B  <->  G : A
--> B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    C_ wss 3263   ran crn 4819    Fn wfn 5389   -->wf 5390
This theorem is referenced by:  feq1d  5520  feq1i  5525  elimf  5530  f00  5568  fconstg  5570  f1eq1  5574  fconst2g  5885  fconstfv  5893  elmapg  6967  ac6sfi  7287  ac5num  7850  acni2  7860  cofsmo  8082  cfsmolem  8083  cfcoflem  8085  coftr  8086  alephsing  8089  axdc2lem  8261  axdc3lem2  8264  axdc3lem3  8265  axdc3  8267  axdc4lem  8268  ac6num  8292  inar1  8583  1fv  11050  axdc4uzlem  11248  seqf1olem2  11290  seqf1o  11291  iswrd  11656  ramub2  13309  ramcl  13324  isacs2  13805  isacs1i  13809  mreacs  13810  isgrpinv  14782  isghm  14933  1stcfb  17429  upxp  17576  txcn  17579  isi1f  19433  mbfi1fseqlem6  19479  mbfi1flimlem  19481  itg2addlem  19517  plyf  19984  iseupa  21535  isgrpo  21632  ismgm  21756  elghomlem2  21798  vci  21875  isvclem  21904  isnvlem  21937  ajmoi  22208  ajval  22211  hlimi  22538  chlimi  22585  chcompl  22593  adjmo  23183  adjeu  23240  adjval  23241  adj1  23284  adjeq  23286  cnlnssadj  23431  pjinvari  23542  isrnmeas  24350  fprb  25153  orderseqlem  25276  soseq  25278  elno  25324  volsupnfl  25956  filnetlem4  26101  upixp  26122  sdclem2  26137  sdclem1  26138  fdc  26140  ismrc  26446  islindf  26951  fmuldfeqlem1  27380  fmuldfeq  27381  stoweidlem15  27432  stoweidlem16  27433  stoweidlem17  27434  stoweidlem19  27436  stoweidlem20  27437  stoweidlem21  27438  stoweidlem22  27439  stoweidlem23  27440  stoweidlem27  27444  stoweidlem31  27448  stoweidlem32  27449  stoweidlem42  27459  stoweidlem48  27465  stoweidlem51  27468  stoweidlem59  27476  istendo  30874
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154  df-opab 4208  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-fun 5396  df-fn 5397  df-f 5398
  Copyright terms: Public domain W3C validator