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

Theorem feq12d 5548
Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypotheses
Ref Expression
feq12d.1  |-  ( ph  ->  F  =  G )
feq12d.2  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
feq12d  |-  ( ph  ->  ( F : A --> C 
<->  G : B --> C ) )

Proof of Theorem feq12d
StepHypRef Expression
1 feq12d.1 . . 3  |-  ( ph  ->  F  =  G )
21feq1d 5546 . 2  |-  ( ph  ->  ( F : A --> C 
<->  G : A --> C ) )
3 feq12d.2 . . 3  |-  ( ph  ->  A  =  B )
43feq2d 5547 . 2  |-  ( ph  ->  ( G : A --> C 
<->  G : B --> C ) )
52, 4bitrd 253 1  |-  ( ph  ->  ( F : A --> C 
<->  G : B --> C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369   -->wf 5414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-opab 4351  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-fun 5420  df-fn 5421  df-f 5422
This theorem is referenced by:  feq123d  5549  fprg  5891  smoeq  6811  oif  7744  catcisolem  14974  hofcl  15069  dmdprd  16480  dpjf  16556  pjf2  18139  lmbr2  18863  lmff  18905  dfac14  19191  lmmbr2  20770  lmcau  20823  perfdvf  21378  dvnfre  21426  dvle  21479  dvfsumle  21493  dvfsumge  21494  dvmptrecl  21496  isumgra  23249  iswlk  23426  istrl  23436  constr1trl  23487  constr3trllem1  23536  eupap1  23597  resf1o  26030  ismeas  26613  mbfresfi  28438  sdclem1  28639  dfac21  29419  mat1dimmul  30872
  Copyright terms: Public domain W3C validator