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

Theorem feq12d 6000
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 5997 . 2 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐴𝐶))
3 feq12d.2 . . 3 (𝜑𝐴 = 𝐵)
43feq2d 5998 . 2 (𝜑 → (𝐺:𝐴𝐶𝐺:𝐵𝐶))
52, 4bitrd 268 1 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wf 5853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-fun 5859  df-fn 5860  df-f 5861
This theorem is referenced by:  feq123d  6001  fprg  6387  smoeq  7407  oif  8395  1fv  12415  catcisolem  16696  hofcl  16839  dmdprd  18337  dpjf  18396  pjf2  19998  mat1dimmul  20222  lmbr2  21003  lmff  21045  dfac14  21361  lmmbr2  22997  lmcau  23051  perfdvf  23607  dvnfre  23655  dvle  23708  dvfsumle  23722  dvfsumge  23723  dvmptrecl  23725  uhgr0e  25896  uhgrstrrepe  25903  incistruhgr  25904  upgr1e  25937  1hevtxdg1  26322  umgr2v2e  26341  iswlk  26410  0wlkons1  26882  resf1o  29389  ismeas  30085  omsmeas  30208  mbfresfi  33127  sdclem1  33210  dfac21  37155  fnlimfvre  39342  fourierdlem74  39734  fourierdlem103  39763  fourierdlem104  39764  sge0iunmpt  39972  ismea  40005  isome  40045  sssmf  40284  smflimlem3  40318  smflimlem4  40319  isupwlk  41035
  Copyright terms: Public domain W3C validator