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

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

Proof of Theorem feq1
StepHypRef Expression
1 fneq1 5875 . . 3 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
2 rneq 5255 . . . 4 (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
32sseq1d 3590 . . 3 (𝐹 = 𝐺 → (ran 𝐹𝐵 ↔ ran 𝐺𝐵))
41, 3anbi12d 742 . 2 (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵)))
5 df-f 5790 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
6 df-f 5790 . 2 (𝐺:𝐴𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵))
74, 5, 63bitr4g 301 1 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wss 3535  ran crn 5025   Fn wfn 5781  wf 5782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-br 4574  df-opab 4634  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-fun 5788  df-fn 5789  df-f 5790
This theorem is referenced by:  feq1d  5925  feq1i  5931  elimf  5939  f00  5981  f0bi  5982  f0dom0  5983  fconstg  5986  f1eq1  5990  fconst2g  6347  fsnex  6412  elmapg  7730  ac6sfi  8062  ac5num  8715  acni2  8725  cofsmo  8947  cfsmolem  8948  cfcoflem  8950  coftr  8951  alephsing  8954  axdc2lem  9126  axdc3lem2  9129  axdc3lem3  9130  axdc3  9132  axdc4lem  9133  ac6num  9157  inar1  9449  axdc4uzlem  12595  seqf1olem2  12654  seqf1o  12655  iswrd  13104  cshf1  13349  wrdlen2i  13476  ramub2  15498  ramcl  15513  isacs2  16079  isacs1i  16083  mreacs  16084  mgmb1mgm1  17019  isgrpinv  17237  isghm  17425  islindf  19908  mat1dimelbas  20034  1stcfb  20996  upxp  21174  txcn  21177  isi1f  23160  mbfi1fseqlem6  23206  mbfi1flimlem  23208  itg2addlem  23244  plyf  23671  wlkelwrd  25820  iseupa  26254  isgrpo  26497  vciOLD  26565  isvclem  26594  isnvlem  26629  ajmoi  26900  ajval  26903  hlimi  27231  chlimi  27277  chcompl  27285  adjmo  27877  adjeu  27934  adjval  27935  adj1  27978  adjeq  27980  cnlnssadj  28125  pjinvari  28236  padct  28687  locfinref  29038  isrnmeas  29392  fprb  30718  orderseqlem  30795  soseq  30797  elno  30845  filnetlem4  31348  bj-finsumval0  32123  poimirlem25  32403  poimirlem28  32406  volsupnfl  32423  mbfresfi  32425  upixp  32493  sdclem2  32507  sdclem1  32508  fdc  32510  ismgmOLD  32618  elghomlem2OLD  32654  istendo  34865  ismrc  36081  fmuldfeqlem1  38449  fmuldfeq  38450  dvnprodlem1  38636  stoweidlem15  38708  stoweidlem16  38709  stoweidlem17  38710  stoweidlem19  38712  stoweidlem20  38713  stoweidlem21  38714  stoweidlem22  38715  stoweidlem23  38716  stoweidlem27  38720  stoweidlem31  38724  stoweidlem32  38725  stoweidlem42  38735  stoweidlem48  38741  stoweidlem51  38744  stoweidlem59  38752  isomenndlem  39220  griedg0prc  40486  lincdifsn  42005
  Copyright terms: Public domain W3C validator