Theorem feq23d 6665

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 6659	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:𝐶⟶𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  nvof1o  7236  axdc4uz  13919  isacs  17586  isfunc  17800  funcres  17832  funcpropd  17838  estrcco  18065  funcestrcsetclem9  18083  fullestrcsetc  18086  fullsetcestrc  18101  1stfcl  18132  2ndfcl  18133  evlfcl  18157  curf1cl  18163  yonedalem3b  18214  intopsn  18591  mgmhmpropd  18635  mhmpropd  18729  isghm  19156  pwssplit1  21023  islindf  21779  evls1sca  22279  rrxds  25361  wlkp1  29765  acunirnmpt  32748  fnpreimac  32759  pwrssmgc  33092  cnmbfm  34440  elmrsubrn  35733  poimirlem3  37871  poimirlem28  37896  isrngod  38146  rngosn3  38172  isgrpda  38203  islfld  39435  tendofset  41131  tendoset  41132  sn-isghm  43028  mapfzcons  43070  diophrw  43113  refsum2cnlem1  45394  funcringcsetcALTV2lem9  48655  funcringcsetclem9ALTV  48678  termcfuncval  49888  aacllem  50157