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

Theorem feq23d 5469
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 2359 . 2  |-  ( ph  ->  F  =  F )
2 feq23d.1 . 2  |-  ( ph  ->  A  =  C )
3 feq23d.2 . 2  |-  ( ph  ->  B  =  D )
41, 2, 3feq123d 5464 1  |-  ( ph  ->  ( F : A --> B 
<->  F : C --> D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1642   -->wf 5333
This theorem is referenced by:  axdc4uz  11137  isacs  13652  isfunc  13837  funcres  13869  funcpropd  13873  funcres2c  13874  catciso  14038  1stfcl  14070  2ndfcl  14071  evlfcl  14095  curf1cl  14101  yonedalem4c  14150  yonedalem3b  14152  yonedainv  14154  mhmpropd  14520  iscau  18806  isgrp2d  21014  isgrpda  21076  isrngo  21157  isrngod  21158  rngosn3  21205  ajfval  21501  cnmbfm  23877  orvcval4  23967  mapfzcons  26116  diophrw  26161  pwssplit1  26511  islindf  26605  refsum2cnlem1  27031  islfld  29321  tendofset  31016  tendoset  31017
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4105  df-opab 4159  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-fun 5339  df-fn 5340  df-f 5341
  Copyright terms: Public domain W3C validator