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

Theorem feq12d 5929
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 5926 . 2 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐴𝐶))
3 feq12d.2 . . 3 (𝜑𝐴 = 𝐵)
43feq2d 5927 . 2 (𝜑 → (𝐺:𝐴𝐶𝐺:𝐵𝐶))
52, 4bitrd 266 1 (𝜑 → (𝐹:𝐴𝐶𝐺:𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wf 5783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575  df-opab 4635  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-fun 5789  df-fn 5790  df-f 5791
This theorem is referenced by:  feq123d  5930  fprg  6302  smoeq  7308  oif  8292  1fv  12279  catcisolem  16522  hofcl  16665  dmdprd  18163  dpjf  18222  pjf2  19816  mat1dimmul  20040  lmbr2  20812  lmff  20854  dfac14  21170  lmmbr2  22780  lmcau  22833  perfdvf  23387  dvnfre  23435  dvle  23488  dvfsumle  23502  dvfsumge  23503  dvmptrecl  23505  uhgrac  25597  isumgra  25607  iswlk  25811  istrl  25830  constr1trl  25881  constr3trllem1  25941  eupap1  26266  resf1o  28696  ismeas  29392  omsmeas  29515  mbfresfi  32426  sdclem1  32509  dfac21  36454  fnlimfvre  38542  fourierdlem74  38874  fourierdlem103  38903  fourierdlem104  38904  sge0iunmpt  39112  ismea  39145  isome  39185  sssmf  39426  smflimlem3  39460  smflimlem4  39461  uhgr0e  40295  uhgrstrrepe  40303  incistruhgr  40304  upgr1e  40337  1hevtxdg1  40720  umgr2v2e  40740  is1wlk  40812  isWlk  40813  0wlkOns1  41288
  Copyright terms: Public domain W3C validator