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

Theorem feq23d 5591
Description: Equality deduction for functions. (Contributed by NM, 8-Jun-2013.)
Hypotheses
Ref Expression
feq23d.1  |-  ( ph  ->  A  =  C )
feq23d.2  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
feq23d  |-  ( ph  ->  ( F : A --> B 
<->  F : C --> D ) )

Proof of Theorem feq23d
StepHypRef Expression
1 eqidd 2439 . 2  |-  ( ph  ->  F  =  F )
2 feq23d.1 . 2  |-  ( ph  ->  A  =  C )
3 feq23d.2 . 2  |-  ( ph  ->  B  =  D )
41, 2, 3feq123d 5586 1  |-  ( ph  ->  ( F : A --> B 
<->  F : C --> D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653   -->wf 5453
This theorem is referenced by:  axdc4uz  11327  isacs  13881  isfunc  14066  funcres  14098  funcpropd  14102  funcres2c  14103  catciso  14267  1stfcl  14299  2ndfcl  14300  evlfcl  14324  curf1cl  14330  yonedalem4c  14379  yonedalem3b  14381  yonedainv  14383  mhmpropd  14749  isgrp2d  21828  isgrpda  21890  isrngod  21972  rngosn3  22019  ajfval  22315  nvof1o  24045  rrhf  24386  cnmbfm  24618  orvcval4  24723  mapfzcons  26786  diophrw  26831  pwssplit1  27179  islindf  27273  refsum2cnlem1  27698  islfld  29934  tendofset  31629  tendoset  31630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216  df-opab 4270  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-fun 5459  df-fn 5460  df-f 5461
  Copyright terms: Public domain W3C validator