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

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

Proof of Theorem feq1
StepHypRef Expression
1 fneq1 6017 . . 3 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
2 rneq 5383 . . . 4 (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
32sseq1d 3665 . . 3 (𝐹 = 𝐺 → (ran 𝐹𝐵 ↔ ran 𝐺𝐵))
41, 3anbi12d 747 . 2 (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵)))
5 df-f 5930 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
6 df-f 5930 . 2 (𝐺:𝐴𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵))
74, 5, 63bitr4g 303 1 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wss 3607  ran crn 5144   Fn wfn 5921  wf 5922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-fun 5928  df-fn 5929  df-f 5930
This theorem is referenced by:  feq1d  6068  feq1i  6074  elimf  6082  f00  6125  f0bi  6126  f0dom0  6127  fconstg  6130  f1eq1  6134  fconst2g  6509  fsnex  6578  elmapg  7912  ac6sfi  8245  ac5num  8897  acni2  8907  cofsmo  9129  cfsmolem  9130  cfcoflem  9132  coftr  9133  alephsing  9136  axdc2lem  9308  axdc3lem2  9311  axdc3lem3  9312  axdc3  9314  axdc4lem  9315  ac6num  9339  inar1  9635  axdc4uzlem  12822  seqf1olem2  12881  seqf1o  12882  iswrd  13339  cshf1  13602  wrdlen2i  13732  ramub2  15765  ramcl  15780  isacs2  16361  isacs1i  16365  mreacs  16366  mgmb1mgm1  17301  isgrpinv  17519  isghm  17707  islindf  20199  mat1dimelbas  20325  1stcfb  21296  upxp  21474  txcn  21477  isi1f  23486  mbfi1fseqlem6  23532  mbfi1flimlem  23534  itg2addlem  23570  plyf  23999  griedg0prc  26201  isgrpo  27479  vciOLD  27544  isvclem  27560  isnvlem  27593  ajmoi  27842  ajval  27845  hlimi  28173  chlimi  28219  chcompl  28227  adjmo  28819  adjeu  28876  adjval  28877  adj1  28920  adjeq  28922  cnlnssadj  29067  pjinvari  29178  padct  29625  locfinref  30036  isrnmeas  30391  fprb  31795  orderseqlem  31877  soseq  31879  elno  31924  filnetlem4  32501  bj-finsumval0  33277  poimirlem25  33564  poimirlem28  33567  volsupnfl  33584  mbfresfi  33586  upixp  33654  sdclem2  33668  sdclem1  33669  fdc  33671  ismgmOLD  33779  elghomlem2OLD  33815  istendo  36365  ismrc  37581  fmuldfeqlem1  40132  fmuldfeq  40133  dvnprodlem1  40479  stoweidlem15  40550  stoweidlem16  40551  stoweidlem17  40552  stoweidlem19  40554  stoweidlem20  40555  stoweidlem21  40556  stoweidlem22  40557  stoweidlem23  40558  stoweidlem27  40562  stoweidlem31  40566  stoweidlem32  40567  stoweidlem42  40577  stoweidlem48  40583  stoweidlem51  40586  stoweidlem59  40594  isomenndlem  41065  smfpimcclem  41334  lincdifsn  42538
  Copyright terms: Public domain W3C validator