Theorem feq23d 6511

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ⟶wf 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-fun 6359  df-fn 6360  df-f 6361

This theorem is referenced by:  nvof1o  7039  axdc4uz  13355  isacs  16924  isfunc  17136  funcres  17168  funcpropd  17172  estrcco  17382  funcestrcsetclem9  17400  fullestrcsetc  17403  fullsetcestrc  17418  1stfcl  17449  2ndfcl  17450  evlfcl  17474  curf1cl  17480  yonedalem3b  17531  intopsn  17866  mhmpropd  17964  pwssplit1  19833  evls1sca  20488  islindf  20958  rrxds  23998  wlkp1  27465  acunirnmpt  30406  fnpreimac  30418  cnmbfm  31523  elmrsubrn  32769  poimirlem3  34897  poimirlem28  34922  isrngod  35178  rngosn3  35204  isgrpda  35235  islfld  36200  tendofset  37896  tendoset  37897  mapfzcons  39320  diophrw  39363  refsum2cnlem1  41301  mgmhmpropd  44059  funcringcsetcALTV2lem9  44322  funcringcsetclem9ALTV  44345  aacllem  44909