Theorem feq23d 6711

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 2728	. 2 ⊢ (𝜑 → 𝐹 = 𝐹)
2		feq23d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
3		feq23d.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
4	1, 2, 3	feq123d 6705	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534  ⟶wf 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143  df-opab 5205  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-fun 6544  df-fn 6545  df-f 6546

This theorem is referenced by:  nvof1o  7283  axdc4uz  13973  isacs  17622  isfunc  17841  funcres  17873  funcpropd  17880  estrcco  18111  funcestrcsetclem9  18130  fullestrcsetc  18133  fullsetcestrc  18148  1stfcl  18179  2ndfcl  18180  evlfcl  18205  curf1cl  18211  yonedalem3b  18262  intopsn  18605  mgmhmpropd  18649  mhmpropd  18740  pwssplit1  20933  islindf  21733  evls1sca  22229  rrxds  25308  wlkp1  29482  acunirnmpt  32428  fnpreimac  32440  pwrssmgc  32709  cnmbfm  33819  elmrsubrn  35066  poimirlem3  37031  poimirlem28  37056  isrngod  37306  rngosn3  37332  isgrpda  37363  islfld  38471  tendofset  40168  tendoset  40169  mapfzcons  42058  diophrw  42101  refsum2cnlem1  44322  funcringcsetcALTV2lem9  47283  funcringcsetclem9ALTV  47306  aacllem  48157