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

Theorem feq1 5568
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 5526 . . 3  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )
2 rneq 5087 . . . 4  |-  ( F  =  G  ->  ran  F  =  ran  G )
32sseq1d 3367 . . 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 5450 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
6 df-f 5450 . 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 1652    C_ wss 3312   ran crn 4871    Fn wfn 5441   -->wf 5442
This theorem is referenced by:  feq1d  5572  feq1i  5577  elimf  5582  f00  5620  fconstg  5622  f1eq1  5626  fconst2g  5938  fconstfv  5946  elmapg  7023  ac6sfi  7343  ac5num  7909  acni2  7919  cofsmo  8141  cfsmolem  8142  cfcoflem  8144  coftr  8145  alephsing  8148  axdc2lem  8320  axdc3lem2  8323  axdc3lem3  8324  axdc3  8326  axdc4lem  8327  ac6num  8351  inar1  8642  1fv  11112  axdc4uzlem  11313  seqf1olem2  11355  seqf1o  11356  iswrd  11721  ramub2  13374  ramcl  13389  isacs2  13870  isacs1i  13874  mreacs  13875  isgrpinv  14847  isghm  14998  1stcfb  17500  upxp  17647  txcn  17650  isi1f  19558  mbfi1fseqlem6  19604  mbfi1flimlem  19606  itg2addlem  19642  plyf  20109  iseupa  21679  isgrpo  21776  ismgm  21900  elghomlem2  21942  vci  22019  isvclem  22048  isnvlem  22081  ajmoi  22352  ajval  22355  hlimi  22682  chlimi  22729  chcompl  22737  adjmo  23327  adjeu  23384  adjval  23385  adj1  23428  adjeq  23430  cnlnssadj  23575  pjinvari  23686  isrnmeas  24546  fprb  25389  orderseqlem  25519  soseq  25521  elno  25593  volsupnfl  26241  mbfresfi  26243  filnetlem4  26401  upixp  26422  sdclem2  26437  sdclem1  26438  fdc  26440  ismrc  26746  islindf  27250  fmuldfeqlem1  27679  fmuldfeq  27680  stoweidlem15  27731  stoweidlem16  27732  stoweidlem17  27733  stoweidlem19  27735  stoweidlem20  27736  stoweidlem21  27737  stoweidlem22  27738  stoweidlem23  27739  stoweidlem27  27743  stoweidlem31  27747  stoweidlem32  27748  stoweidlem42  27758  stoweidlem48  27764  stoweidlem51  27767  stoweidlem59  27775  istendo  31494
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-fun 5448  df-fn 5449  df-f 5450
  Copyright terms: Public domain W3C validator