Theorem feq23d 6651

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-fun 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  nvof1o  7221  axdc4uz  13909  isacs  17575  isfunc  17789  funcres  17821  funcpropd  17827  estrcco  18054  funcestrcsetclem9  18072  fullestrcsetc  18075  fullsetcestrc  18090  1stfcl  18121  2ndfcl  18122  evlfcl  18146  curf1cl  18152  yonedalem3b  18203  intopsn  18546  mgmhmpropd  18590  mhmpropd  18684  isghm  19112  pwssplit1  20981  islindf  21737  evls1sca  22226  rrxds  25309  wlkp1  29643  acunirnmpt  32616  fnpreimac  32628  pwrssmgc  32955  cnmbfm  34233  elmrsubrn  35495  poimirlem3  37605  poimirlem28  37630  isrngod  37880  rngosn3  37906  isgrpda  37937  islfld  39043  tendofset  40740  tendoset  40741  sn-isghm  42649  mapfzcons  42692  diophrw  42735  refsum2cnlem1  45018  funcringcsetcALTV2lem9  48286  funcringcsetclem9ALTV  48309  termcfuncval  49521  aacllem  49790