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

Theorem feq12d 6475
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 6472 . 2 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐴𝐶))
3 feq12d.2 . . 3 (𝜑𝐴 = 𝐵)
43feq2d 6473 . 2 (𝜑 → (𝐺:𝐴𝐶𝐺:𝐵𝐶))
52, 4bitrd 282 1 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wf 6320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-fun 6326  df-fn 6327  df-f 6328
This theorem is referenced by:  feq123d  6476  fprg  6894  smoeq  7970  oif  8978  1fv  13021  catcisolem  17358  hofcl  17501  dmdprd  19113  dpjf  19172  pjf2  20403  mat1dimmul  21081  lmbr2  21864  lmff  21906  dfac14  22223  lmmbr2  23863  lmcau  23917  perfdvf  24506  dvnfre  24555  dvle  24610  dvfsumle  24624  dvfsumge  24625  dvmptrecl  24627  uhgr0e  26864  uhgrstrrepe  26871  incistruhgr  26872  upgr1e  26906  1hevtxdg1  27296  umgr2v2e  27315  iswlk  27400  0wlkons1  27906  resf1o  30492  ismeas  31568  omsmeas  31691  breprexplema  32011  satfun  32768  mbfresfi  35100  sdclem1  35178  dfac21  40005  fnlimfvre  42311  climrescn  42385  fourierdlem74  42817  fourierdlem103  42846  fourierdlem104  42847  sge0iunmpt  43052  ismea  43085  isome  43128  sssmf  43367  smflimlem3  43401  smflimlem4  43402  isupwlk  44359
  Copyright terms: Public domain W3C validator