Theorem feq23d 5728

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

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1446   -->wf 5581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-br 4406  df-opab 4465  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-fun 5587  df-fn 5588  df-f 5589

This theorem is referenced by:  nvof1o  6184  axdc4uz  12203  isacs  15569  isfunc  15781  funcres  15813  funcpropd  15817  estrcco  16027  funcestrcsetclem9  16045  fullestrcsetc  16048  fullsetcestrc  16063  1stfcl  16094  2ndfcl  16095  evlfcl  16119  curf1cl  16125  yonedalem3b  16176  intopsn  16510  mhmpropd  16600  pwssplit1  18294  evls1sca  18924  islindf  19382  rrxds  22364  isgrp2d  25975  isgrpda  26037  isrngod  26119  rngosn3  26166  acunirnmpt  28273  cnmbfm  29097  elmrsubrn  30170  poimirlem3  31955  poimirlem28  31980  islfld  32640  tendofset  34337  tendoset  34338  mapfzcons  35570  diophrw  35613  refsum2cnlem1  37368  mgmhmpropd  39889  funcringcsetcALTV2lem9  40150  funcringcsetclem9ALTV  40173  aacllem  40644