Theorem feq23d 6702

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-fun 6540  df-fn 6541  df-f 6542

This theorem is referenced by:  nvof1o  7280  axdc4uz  14022  isacs  17708  isfunc  17922  funcres  17954  funcpropd  17960  estrcco  18187  funcestrcsetclem9  18205  fullestrcsetc  18208  fullsetcestrc  18223  1stfcl  18254  2ndfcl  18255  evlfcl  18279  curf1cl  18285  yonedalem3b  18336  intopsn  18713  mgmhmpropd  18757  mhmpropd  18851  isghm  19287  pwssplit1  21161  islindf  21943  evls1sca  22464  rrxds  25533  wlkp1  30010  acunirnmpt  32985  fnpreimac  32996  pwrssmgc  33301  cnmbfm  34634  elmrsubrn  35993  poimirlem3  38255  poimirlem28  38280  isrngod  38530  rngosn3  38556  isgrpda  38587  islfld  39817  tendofset  41513  tendoset  41514  sn-isghm  43388  mapfzcons  43430  diophrw  43473  refsum2cnlem1  45740  funcringcsetcALTV2lem9  49046  funcringcsetclem9ALTV  49069  termcfuncval  50293  aacllem  50584