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

Theorem feq1 6013
Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
feq1 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))

Proof of Theorem feq1
StepHypRef Expression
1 fneq1 5967 . . 3 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
2 rneq 5340 . . . 4 (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
32sseq1d 3624 . . 3 (𝐹 = 𝐺 → (ran 𝐹𝐵 ↔ ran 𝐺𝐵))
41, 3anbi12d 746 . 2 (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵)))
5 df-f 5880 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
6 df-f 5880 . 2 (𝐺:𝐴𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵))
74, 5, 63bitr4g 303 1 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wss 3567  ran crn 5105   Fn wfn 5871  wf 5872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-fun 5878  df-fn 5879  df-f 5880
This theorem is referenced by:  feq1d  6017  feq1i  6023  elimf  6031  f00  6074  f0bi  6075  f0dom0  6076  fconstg  6079  f1eq1  6083  fconst2g  6453  fsnex  6523  elmapg  7855  ac6sfi  8189  ac5num  8844  acni2  8854  cofsmo  9076  cfsmolem  9077  cfcoflem  9079  coftr  9080  alephsing  9083  axdc2lem  9255  axdc3lem2  9258  axdc3lem3  9259  axdc3  9261  axdc4lem  9262  ac6num  9286  inar1  9582  axdc4uzlem  12765  seqf1olem2  12824  seqf1o  12825  iswrd  13290  cshf1  13537  wrdlen2i  13667  ramub2  15699  ramcl  15714  isacs2  16295  isacs1i  16299  mreacs  16300  mgmb1mgm1  17235  isgrpinv  17453  isghm  17641  islindf  20132  mat1dimelbas  20258  1stcfb  21229  upxp  21407  txcn  21410  isi1f  23422  mbfi1fseqlem6  23468  mbfi1flimlem  23470  itg2addlem  23506  plyf  23935  griedg0prc  26137  isgrpo  27321  vciOLD  27386  isvclem  27402  isnvlem  27435  ajmoi  27684  ajval  27687  hlimi  28015  chlimi  28061  chcompl  28069  adjmo  28661  adjeu  28718  adjval  28719  adj1  28762  adjeq  28764  cnlnssadj  28909  pjinvari  29020  padct  29471  locfinref  29882  isrnmeas  30237  fprb  31645  orderseqlem  31723  soseq  31725  elno  31773  filnetlem4  32351  bj-finsumval0  33118  poimirlem25  33405  poimirlem28  33408  volsupnfl  33425  mbfresfi  33427  upixp  33495  sdclem2  33509  sdclem1  33510  fdc  33512  ismgmOLD  33620  elghomlem2OLD  33656  istendo  35867  ismrc  37083  fmuldfeqlem1  39614  fmuldfeq  39615  dvnprodlem1  39924  stoweidlem15  39995  stoweidlem16  39996  stoweidlem17  39997  stoweidlem19  39999  stoweidlem20  40000  stoweidlem21  40001  stoweidlem22  40002  stoweidlem23  40003  stoweidlem27  40007  stoweidlem31  40011  stoweidlem32  40012  stoweidlem42  40022  stoweidlem48  40028  stoweidlem51  40031  stoweidlem59  40039  isomenndlem  40507  smfpimcclem  40776  lincdifsn  41978
  Copyright terms: Public domain W3C validator