Theorem feq23d 6742

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-fun 6575  df-fn 6576  df-f 6577

This theorem is referenced by:  nvof1o  7316  axdc4uz  14035  isacs  17709  isfunc  17928  funcres  17960  funcpropd  17967  estrcco  18198  funcestrcsetclem9  18217  fullestrcsetc  18220  fullsetcestrc  18235  1stfcl  18266  2ndfcl  18267  evlfcl  18292  curf1cl  18298  yonedalem3b  18349  intopsn  18692  mgmhmpropd  18736  mhmpropd  18827  isghm  19255  pwssplit1  21081  islindf  21855  evls1sca  22348  rrxds  25446  wlkp1  29717  acunirnmpt  32677  fnpreimac  32689  pwrssmgc  32973  cnmbfm  34228  elmrsubrn  35488  poimirlem3  37583  poimirlem28  37608  isrngod  37858  rngosn3  37884  isgrpda  37915  islfld  39018  tendofset  40715  tendoset  40716  sn-isghm  42628  mapfzcons  42672  diophrw  42715  refsum2cnlem1  44937  funcringcsetcALTV2lem9  48021  funcringcsetclem9ALTV  48044  aacllem  48895