Theorem feq23d 6731

Description: Equality deduction for functions. (Contributed by NM, 8-Jun-2013.)

Hypotheses

Ref	Expression
feq23d.1	⊢ (𝜑 → 𝐴 = 𝐶)
feq23d.2	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
feq23d	⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷))

Proof of Theorem feq23d

Step	Hyp	Ref	Expression
1		eqidd 2738	. 2 ⊢ (𝜑 → 𝐹 = 𝐹)
2		feq23d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
3		feq23d.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
4	1, 2, 3	feq123d 6725	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ⟶wf 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-fun 6563  df-fn 6564  df-f 6565

This theorem is referenced by:  nvof1o  7300  axdc4uz  14025  isacs  17694  isfunc  17909  funcres  17941  funcpropd  17947  estrcco  18174  funcestrcsetclem9  18193  fullestrcsetc  18196  fullsetcestrc  18211  1stfcl  18242  2ndfcl  18243  evlfcl  18267  curf1cl  18273  yonedalem3b  18324  intopsn  18667  mgmhmpropd  18711  mhmpropd  18805  isghm  19233  pwssplit1  21058  islindf  21832  evls1sca  22327  rrxds  25427  wlkp1  29699  acunirnmpt  32669  fnpreimac  32681  pwrssmgc  32990  cnmbfm  34265  elmrsubrn  35525  poimirlem3  37630  poimirlem28  37655  isrngod  37905  rngosn3  37931  isgrpda  37962  islfld  39063  tendofset  40760  tendoset  40761  sn-isghm  42683  mapfzcons  42727  diophrw  42770  refsum2cnlem1  45042  funcringcsetcALTV2lem9  48214  funcringcsetclem9ALTV  48237  aacllem  49320