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

Theorem feq12d 6588
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 6585 . 2 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐴𝐶))
3 feq12d.2 . . 3 (𝜑𝐴 = 𝐵)
43feq2d 6586 . 2 (𝜑 → (𝐺:𝐴𝐶𝐺:𝐵𝐶))
52, 4bitrd 278 1 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1539  wf 6429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-fun 6435  df-fn 6436  df-f 6437
This theorem is referenced by:  feq123d  6589  fprg  7027  smoeq  8181  oif  9289  1fv  13375  catcisolem  17825  hofcl  17977  dmdprd  19601  dpjf  19660  pjf2  20921  mat1dimmul  21625  lmbr2  22410  lmff  22452  dfac14  22769  lmmbr2  24423  lmcau  24477  perfdvf  25067  dvnfre  25116  dvle  25171  dvfsumle  25185  dvfsumge  25186  dvmptrecl  25188  uhgr0e  27441  uhgrstrrepe  27448  incistruhgr  27449  upgr1e  27483  1hevtxdg1  27873  umgr2v2e  27892  iswlk  27977  0wlkons1  28485  resf1o  31065  ismeas  32167  omsmeas  32290  breprexplema  32610  satfun  33373  mbfresfi  35823  sdclem1  35901  dfac21  40891  fnlimfvre  43215  climrescn  43289  fourierdlem74  43721  fourierdlem103  43750  fourierdlem104  43751  sge0iunmpt  43956  ismea  43989  isome  44032  sssmf  44274  smflimlem3  44308  smflimlem4  44309  isupwlk  45298
  Copyright terms: Public domain W3C validator