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

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

Proof of Theorem feq1
StepHypRef Expression
1 fneq1 6190 . . 3 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
2 rneq 5552 . . . 4 (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
32sseq1d 3829 . . 3 (𝐹 = 𝐺 → (ran 𝐹𝐵 ↔ ran 𝐺𝐵))
41, 3anbi12d 618 . 2 (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵)))
5 df-f 6105 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
6 df-f 6105 . 2 (𝐺:𝐴𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵))
74, 5, 63bitr4g 305 1 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wss 3769  ran crn 5312   Fn wfn 6096  wf 6097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-br 4845  df-opab 4907  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-fun 6103  df-fn 6104  df-f 6105
This theorem is referenced by:  feq1d  6241  feq1i  6247  elimf  6255  f00  6302  f0bi  6303  f0dom0  6304  fconstg  6307  f1eq1  6311  fconst2g  6693  fsnex  6762  elmapg  8105  ac6sfi  8443  updjud  9043  ac5num  9142  acni2  9152  cofsmo  9376  cfsmolem  9377  cfcoflem  9379  coftr  9380  alephsing  9383  axdc2lem  9555  axdc3lem2  9558  axdc3lem3  9559  axdc3  9561  axdc4lem  9562  ac6num  9586  inar1  9882  axdc4uzlem  13006  seqf1olem2  13064  seqf1o  13065  iswrd  13518  cshf1  13780  wrdlen2i  13911  ramub2  15935  ramcl  15950  isacs2  16518  isacs1i  16522  mreacs  16523  mgmb1mgm1  17459  isgrpinv  17677  isghm  17862  islindf  20361  mat1dimelbas  20488  1stcfb  21462  upxp  21640  txcn  21643  isi1f  23655  mbfi1fseqlem6  23701  mbfi1flimlem  23703  itg2addlem  23739  plyf  24168  griedg0prc  26372  isgrpo  27680  vciOLD  27744  isvclem  27760  isnvlem  27793  ajmoi  28042  ajval  28045  hlimi  28373  chlimi  28419  chcompl  28427  adjmo  29019  adjeu  29076  adjval  29077  adj1  29120  adjeq  29122  cnlnssadj  29267  pjinvari  29378  padct  29824  locfinref  30233  isrnmeas  30588  fprb  31991  orderseqlem  32073  soseq  32075  elno  32120  filnetlem4  32697  bj-finsumval0  33464  poimirlem25  33747  poimirlem28  33750  volsupnfl  33767  mbfresfi  33768  upixp  33836  sdclem2  33849  sdclem1  33850  fdc  33852  ismgmOLD  33960  elghomlem2OLD  33996  istendo  36541  ismrc  37766  fmuldfeqlem1  40294  fmuldfeq  40295  dvnprodlem1  40641  stoweidlem15  40711  stoweidlem16  40712  stoweidlem17  40713  stoweidlem19  40715  stoweidlem20  40716  stoweidlem21  40717  stoweidlem22  40718  stoweidlem23  40719  stoweidlem27  40723  stoweidlem31  40727  stoweidlem32  40728  stoweidlem42  40738  stoweidlem48  40744  stoweidlem51  40747  stoweidlem59  40755  isomenndlem  41226  smfpimcclem  41495  lincdifsn  42781
  Copyright terms: Public domain W3C validator