Theorem feq23d 5559

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1369   -->wf 5419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-br 4298  df-opab 4356  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-fun 5425  df-fn 5426  df-f 5427

This theorem is referenced by:  nvof1o  5992  axdc4uz  11810  isacs  14594  isfunc  14779  funcres  14811  funcpropd  14815  funcres2c  14816  catciso  14980  1stfcl  15012  2ndfcl  15013  evlfcl  15037  curf1cl  15043  yonedalem4c  15092  yonedalem3b  15094  yonedainv  15096  mhmpropd  15475  pwssplit1  17145  evls1sca  17763  islindf  18246  rrxds  20902  isgrp2d  23727  isgrpda  23789  isrngod  23871  rngosn3  23918  ajfval  24214  rrhf  26432  cnmbfm  26683  orvcval4  26848  mapfzcons  29057  diophrw  29102  refsum2cnlem1  29764  mdetdiaglem  30940  bj-finsumval0  32588  islfld  32712  tendofset  34407  tendoset  34408