Theorem feq23d 6657

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  nvof1o  7231  axdc4uz  13944  isacs  17615  isfunc  17829  funcres  17861  funcpropd  17867  estrcco  18094  funcestrcsetclem9  18112  fullestrcsetc  18115  fullsetcestrc  18130  1stfcl  18161  2ndfcl  18162  evlfcl  18186  curf1cl  18192  yonedalem3b  18243  intopsn  18620  mgmhmpropd  18664  mhmpropd  18758  isghm  19188  pwssplit1  21056  islindf  21794  evls1sca  22316  rrxds  25385  wlkp1  29773  acunirnmpt  32758  fnpreimac  32769  pwrssmgc  33086  cnmbfm  34454  elmrsubrn  35755  poimirlem3  37997  poimirlem28  38022  isrngod  38272  rngosn3  38298  isgrpda  38329  islfld  39561  tendofset  41257  tendoset  41258  sn-isghm  43130  mapfzcons  43172  diophrw  43215  refsum2cnlem1  45492  funcringcsetcALTV2lem9  48796  funcringcsetclem9ALTV  48819  termcfuncval  50029  aacllem  50298