Theorem fneq1d 6632

Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
fneq1d.1	⊢ (𝜑 → 𝐹 = 𝐺)

Assertion

Ref	Expression
fneq1d	⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Proof of Theorem fneq1d

Step	Hyp	Ref	Expression
1		fneq1d.1	. 2 ⊢ (𝜑 → 𝐹 = 𝐺)
2		fneq1 6630	. 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   Fn wfn 6533

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-fun 6540  df-fn 6541

This theorem is used by:  fneq12d  6634  f1o00  6860  f1oprswap  6870  f1ompt  7111  fmpt2d  7125  f1ocnvd  7672  offn  7706  offval2f  7708  offval2  7713  ofrfval2  7714  caofinvl  7725  f1od2  8110  fsplitfpar  8131  omxpenlem  9100  itunifn  10498  konigthlem  10656  seqof  14205  swrdlen  14799  mptfzshft  15949  prdsdsfn  17641  imasdsfn  17691  cidfn  17858  comffn  17884  isoval  17945  invf1o  17949  isofn  17955  brssc  17994  cofucl  18068  estrchomfn  18314  funcestrcsetclem4  18322  funcsetcestrclem4  18337  1stfcl  18376  2ndfcl  18377  prfcl  18382  evlfcl  18401  curf1cl  18407  curfcl  18411  hofcl  18438  yonedainv  18460  smndex1n0mnd  19116  grpinvf1o  19224  ghmquskerco  19503  pmtrrn  19676  pmtrfrn  19677  rnghmresfn  20876  rhmresfn  20905  rhmsubclem1  20942  srngf1o  21110  ofco2  22771  mat1dimscm  22795  neif  23423  fmf  24269  fncpn  26258  mdeg0  26393  om2noseqfo  28689  noseqrdglem  28696  noseqrdgfn  28697  noseqrdg0  28698  tglnfn  29015  tgplnfn  29258  grpoinvf  31139  kbass2  32724  fnresin  33265  f1o3d  33267  suppovss  33321  prodindf  33475  esplyfval3  34250  frlmdim  34289  pstmxmet  34575  ofcfn  34778  ofcfval2  34782  signstlen  35242  bnj941  35449  satfn  36206  msubrn  36380  poimirlem4  38635  cnambfre  38679  sdclem2  38769  diafn  42184  dibfna  42304  dicfnN  42333  dihf11lem  42416  mapd1o  42798  hdmapfnN  42979  hgmapfnN  43038  aks4d1p1p5  43218  hbtlem7  44220  fsovf1od  45109  ntrrn  45215  ntrf  45216  dssmapntrcls  45221  addrfn  45547  subrfn  45548  mulvfn  45549  fsumsermpt  46684  hoidmvlelem3  47700  smflimsuplem7  47929  tmachlem-extpcover  48048  rhmsubcALTVlem1  49471  funcringcsetcALTV2lem4  49483  funcringcsetclem4ALTV  49506  ackvalsucsucval  49893  sectfn  50236  invfn  50237  isofnALT  50238  iinfssclem2  50262  nelsubclem  50274  upeu4  50405  swapf2fn  50483  fucofn2  50539  fucofn22  50555  fucoppc  50638  veronesevrowd  51147  veronesematrowd  51149