Theorem feq23d 6729

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-fun 6563  df-fn 6564  df-f 6565

This theorem is used by:  nvof1o  7314  axdc4uz  14157  isacs  17857  isfunc  18071  funcres  18103  funcpropd  18109  estrcco  18336  funcestrcsetclem9  18354  fullestrcsetc  18357  fullsetcestrc  18372  1stfcl  18403  2ndfcl  18404  evlfcl  18428  curf1cl  18434  yonedalem3b  18485  intopsn  18864  mgmhmpropd  18919  mhmpropd  19019  isghm  19462  pwssplit1  21367  islindf  22151  evls1sca  22674  rrxds  25747  wlkp1  30293  acunirnmpt  33328  fnpreimac  33339  pwrssmgc  33637  cnmbfm  34978  elmrsubrn  36465  poimirlem3  38746  poimirlem28  38771  isrngod  39035  rngosn3  39061  isgrpda  39092  islfld  40322  tendofset  42018  tendoset  42019  sn-isghm  43888  mapfzcons  43931  diophrw  43974  refsum2cnlem1  46270  funcringcsetcALTV2lem9  49610  funcringcsetclem9ALTV  49633  termcfuncval  50882  aacllem  51251