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

Theorem feq12d 6572
Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypotheses
Ref Expression
feq12d.1 (𝜑𝐹 = 𝐺)
feq12d.2 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
feq12d (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐶))

Proof of Theorem feq12d
StepHypRef Expression
1 feq12d.1 . . 3 (𝜑𝐹 = 𝐺)
21feq1d 6569 . 2 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐴𝐶))
3 feq12d.2 . . 3 (𝜑𝐴 = 𝐵)
43feq2d 6570 . 2 (𝜑 → (𝐺:𝐴𝐶𝐺:𝐵𝐶))
52, 4bitrd 278 1 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1539  wf 6414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-fun 6420  df-fn 6421  df-f 6422
This theorem is referenced by:  feq123d  6573  fprg  7009  smoeq  8152  oif  9219  1fv  13304  catcisolem  17741  hofcl  17893  dmdprd  19516  dpjf  19575  pjf2  20831  mat1dimmul  21533  lmbr2  22318  lmff  22360  dfac14  22677  lmmbr2  24328  lmcau  24382  perfdvf  24972  dvnfre  25021  dvle  25076  dvfsumle  25090  dvfsumge  25091  dvmptrecl  25093  uhgr0e  27344  uhgrstrrepe  27351  incistruhgr  27352  upgr1e  27386  1hevtxdg1  27776  umgr2v2e  27795  iswlk  27880  0wlkons1  28386  resf1o  30967  ismeas  32067  omsmeas  32190  breprexplema  32510  satfun  33273  mbfresfi  35750  sdclem1  35828  dfac21  40807  fnlimfvre  43105  climrescn  43179  fourierdlem74  43611  fourierdlem103  43640  fourierdlem104  43641  sge0iunmpt  43846  ismea  43879  isome  43922  sssmf  44161  smflimlem3  44195  smflimlem4  44196  isupwlk  45186
  Copyright terms: Public domain W3C validator