Theorem feq23d 5724

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 2468	. 2 |- ( ph -> F = F )
2		feq23d.1	. 2 |- ( ph -> A = C )
3		feq23d.2	. 2 |- ( ph -> B = D )
4	1, 2, 3	feq123d 5719	1 |- ( ph -> ( F : A --> B <-> F : C --> D ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   -->wf 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-fun 5588  df-fn 5589  df-f 5590

This theorem is referenced by:  nvof1o  6172  axdc4uz  12057  isacs  14902  isfunc  15087  funcres  15119  funcpropd  15123  funcres2c  15124  catciso  15288  1stfcl  15320  2ndfcl  15321  evlfcl  15345  curf1cl  15351  yonedalem4c  15400  yonedalem3b  15402  yonedainv  15404  mhmpropd  15783  pwssplit1  17488  evls1sca  18131  islindf  18614  scmatmhm  18803  mdetdiaglem  18867  rrxds  21560  isgrp2d  24913  isgrpda  24975  isrngod  25057  rngosn3  25104  ajfval  25400  rrhf  27615  cnmbfm  27874  orvcval4  28039  mapfzcons  30252  diophrw  30296  refsum2cnlem1  30990  iopmapxp  31960  mgmplusgiop  31961  bj-finsumval0  33735  islfld  33859  tendofset  35554  tendoset  35555