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

Theorem feq12d 6265
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 6262 . 2 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐴𝐶))
3 feq12d.2 . . 3 (𝜑𝐴 = 𝐵)
43feq2d 6263 . 2 (𝜑 → (𝐺:𝐴𝐶𝐺:𝐵𝐶))
52, 4bitrd 271 1 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1658  wf 6118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-rab 3125  df-v 3415  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-nul 4144  df-if 4306  df-sn 4397  df-pr 4399  df-op 4403  df-br 4873  df-opab 4935  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-fun 6124  df-fn 6125  df-f 6126
This theorem is referenced by:  feq123d  6266  fprg  6672  smoeq  7712  oif  8703  1fv  12752  catcisolem  17107  hofcl  17251  dmdprd  18750  dpjf  18809  pjf2  20420  mat1dimmul  20649  lmbr2  21433  lmff  21475  dfac14  21791  lmmbr2  23426  lmcau  23480  perfdvf  24065  dvnfre  24113  dvle  24168  dvfsumle  24182  dvfsumge  24183  dvmptrecl  24185  uhgr0e  26368  uhgrstrrepe  26375  incistruhgr  26376  upgr1e  26410  1hevtxdg1  26803  umgr2v2e  26822  iswlk  26907  0wlkons1  27496  resf1o  30052  ismeas  30806  omsmeas  30929  breprexplema  31256  mbfresfi  33998  sdclem1  34080  dfac21  38478  fnlimfvre  40700  climrescn  40774  fourierdlem74  41190  fourierdlem103  41219  fourierdlem104  41220  sge0iunmpt  41425  ismea  41458  isome  41501  sssmf  41740  smflimlem3  41774  smflimlem4  41775  isupwlk  42563
  Copyright terms: Public domain W3C validator