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

Theorem feq123d 5679
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 )
feq123d.3  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
feq123d  |-  ( ph  ->  ( F : A --> C 
<->  G : B --> D ) )

Proof of Theorem feq123d
StepHypRef Expression
1 feq12d.1 . . 3  |-  ( ph  ->  F  =  G )
2 feq12d.2 . . 3  |-  ( ph  ->  A  =  B )
31, 2feq12d 5678 . 2  |-  ( ph  ->  ( F : A --> C 
<->  G : B --> C ) )
4 feq123d.3 . . 3  |-  ( ph  ->  C  =  D )
54feq3d 5677 . 2  |-  ( ph  ->  ( G : B --> C 
<->  G : B --> D ) )
63, 5bitrd 256 1  |-  ( ph  ->  ( F : A --> C 
<->  G : B --> D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   -->wf 5540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-br 4367  df-opab 4426  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-fun 5546  df-fn 5547  df-f 5548
This theorem is referenced by:  feq123  5680  feq23d  5684  fprg  6032  csbwrdg  12644  funcestrcsetclem8  15975  funcsetcestrclem8  15990  funcsetcestrclem9  15991  evlfcl  16050  yonedalem3a  16102  yonedalem4c  16105  yonedalem3b  16107  yonedainv  16109  iscau  22188  isuhgra  24967  uhgraeq12d  24976  constr3trllem3  25322  isrngo  26048  sseqf  29177  ismfs  30139  isuhgr  38925  uhgreq12g  38932  uhgruhgra  38934  uhgrauhgr  38935  uhgrop  38937  uhgrun  38942  isupgr  38950  isumgr  38959  upgrun  38976  umgrun  38978  isuhgrALTV  39269  uhgeq12gALTV  39273  uhguhgra  39275  uhgrauhg  39276  funcringcsetcALTV2lem8  39636  funcringcsetclem8ALTV  39659
  Copyright terms: Public domain W3C validator