Theorem feq23d 6704

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6540  df-fn 6541  df-f 6542

This theorem is used by:  nvof1o  7288  axdc4uz  14130  isacs  17830  isfunc  18044  funcres  18076  funcpropd  18082  estrcco  18309  funcestrcsetclem9  18327  fullestrcsetc  18330  fullsetcestrc  18345  1stfcl  18376  2ndfcl  18377  evlfcl  18401  curf1cl  18407  yonedalem3b  18458  intopsn  18837  mgmhmpropd  18892  mhmpropd  18992  isghm  19435  pwssplit1  21339  islindf  22123  evls1sca  22646  rrxds  25719  wlkp1  30265  acunirnmpt  33300  fnpreimac  33311  pwrssmgc  33607  cnmbfm  34941  elmrsubrn  36371  poimirlem3  38634  poimirlem28  38659  isrngod  38925  rngosn3  38951  isgrpda  38982  islfld  40212  tendofset  41908  tendoset  41909  sn-isghm  43777  mapfzcons  43820  diophrw  43863  refsum2cnlem1  46147  funcringcsetcALTV2lem9  49488  funcringcsetclem9ALTV  49511  termcfuncval  50760  aacllem  51107