Theorem feq23d 5547

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

Step	Hyp	Ref	Expression
1		eqidd 2405	. 2 |- ( ph -> F = F )
2		feq23d.1	. 2 |- ( ph -> A = C )
3		feq23d.2	. 2 |- ( ph -> B = D )
4	1, 2, 3	feq123d 5542	1 |- ( ph -> ( F : A --> B <-> F : C --> D ) )

Syntax hints:   -> wi 4   <-> wb 177   = wceq 1649   -->wf 5409

This theorem is referenced by:  axdc4uz  11277  isacs  13831  isfunc  14016  funcres  14048  funcpropd  14052  funcres2c  14053  catciso  14217  1stfcl  14249  2ndfcl  14250  evlfcl  14274  curf1cl  14280  yonedalem4c  14329  yonedalem3b  14331  yonedainv  14333  mhmpropd  14699  isgrp2d  21776  isgrpda  21838  isrngod  21920  rngosn3  21967  ajfval  22263  nvof1o  23993  rrhf  24334  cnmbfm  24566  orvcval4  24671  mapfzcons  26662  diophrw  26707  pwssplit1  27056  islindf  27150  refsum2cnlem1  27575  islfld  29545  tendofset  31240  tendoset  31241

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-fun 5415  df-fn 5416  df-f 5417