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

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

Proof of Theorem feq1
StepHypRef Expression
1 fneq1 6420 . . 3 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
2 rneq 5782 . . . 4 (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
32sseq1d 3977 . . 3 (𝐹 = 𝐺 → (ran 𝐹𝐵 ↔ ran 𝐺𝐵))
41, 3anbi12d 632 . 2 (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵)))
5 df-f 6335 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
6 df-f 6335 . 2 (𝐺:𝐴𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺𝐵))
74, 5, 63bitr4g 316 1 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398   = wceq 1537  wss 3913  ran crn 5532   Fn wfn 6326  wf 6327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-br 5043  df-opab 5105  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-fun 6333  df-fn 6334  df-f 6335
This theorem is referenced by:  feq1d  6475  feq1i  6481  elimf  6489  f00  6537  f0bi  6538  f0dom0  6539  fconstg  6542  f1eq1  6546  fprb  6932  fconst2g  6941  fsnex  7016  elmapg  8397  ac6sfi  8740  updjud  9341  ac5num  9440  acni2  9450  cofsmo  9669  cfsmolem  9670  cfcoflem  9672  coftr  9673  alephsing  9676  axdc2lem  9848  axdc3lem2  9851  axdc3lem3  9852  axdc3  9854  axdc4lem  9855  ac6num  9879  inar1  10175  axdc4uzlem  13335  seqf1olem2  13395  seqf1o  13396  iswrd  13848  cshf1  14152  wrdlen2i  14284  ramub2  16328  ramcl  16343  isacs2  16903  isacs1i  16907  mreacs  16908  mgmb1mgm1  17844  elefmndbas2  18018  isgrpinv  18135  isghm  18337  islindf  20932  mat1dimelbas  21056  1stcfb  22029  upxp  22207  txcn  22210  isi1f  24257  mbfi1fseqlem6  24303  mbfi1flimlem  24305  itg2addlem  24341  plyf  24774  griedg0prc  27033  isgrpo  28259  vciOLD  28323  isvclem  28339  isnvlem  28372  ajmoi  28620  ajval  28623  hlimi  28950  chlimi  28996  chcompl  29004  adjmo  29594  adjeu  29651  adjval  29652  adj1  29695  adjeq  29697  cnlnssadj  29842  pjinvari  29953  padct  30442  locfinref  31116  isrnmeas  31467  orderseqlem  33102  soseq  33104  elno  33161  filnetlem4  33737  bj-finsumval0  34584  poimirlem25  34958  poimirlem28  34961  volsupnfl  34978  mbfresfi  34979  upixp  35043  sdclem2  35056  sdclem1  35057  fdc  35059  ismgmOLD  35164  elghomlem2OLD  35200  istendo  37932  ismrc  39435  fmuldfeqlem1  42015  fmuldfeq  42016  dvnprodlem1  42379  stoweidlem15  42448  stoweidlem16  42449  stoweidlem17  42450  stoweidlem19  42452  stoweidlem20  42453  stoweidlem21  42454  stoweidlem22  42455  stoweidlem23  42456  stoweidlem27  42460  stoweidlem31  42464  stoweidlem32  42465  stoweidlem42  42475  stoweidlem48  42481  stoweidlem51  42484  stoweidlem59  42492  isomenndlem  42960  smfpimcclem  43229  lincdifsn  44624
  Copyright terms: Public domain W3C validator