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

Theorem feq123d 5544
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 5543 . 2  |-  ( ph  ->  ( F : A --> C 
<->  G : B --> C ) )
4 feq123d.3 . . 3  |-  ( ph  ->  C  =  D )
5 feq3 5539 . . 3  |-  ( C  =  D  ->  ( G : B --> C  <->  G : B
--> D ) )
64, 5syl 16 . 2  |-  ( ph  ->  ( G : B --> C 
<->  G : B --> D ) )
73, 6bitrd 253 1  |-  ( ph  ->  ( F : A --> C 
<->  G : B --> D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369   -->wf 5409
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 2419
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 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288  df-opab 4346  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-fun 5415  df-fn 5416  df-f 5417
This theorem is referenced by:  feq123  5545  feq23d  5549  fprg  5886  csbwrdg  12249  evlfcl  15024  yonedalem3a  15076  yonedalem4c  15079  yonedalem3b  15081  yonedainv  15083  iscau  20762  isuhgra  23188  uhgraeq12d  23192  constr3trllem3  23489  isrngo  23816  sseqf  26727
  Copyright terms: Public domain W3C validator