Theorem fneq1d 6636

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 6634	. 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   Fn wfn 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-fun 6538  df-fn 6539

This theorem is referenced by:  fneq12d  6638  f1o00  6858  f1oprswap  6867  f1ompt  7106  fmpt2d  7119  f1ocnvd  7663  offn  7689  offval2f  7691  offval2  7696  ofrfval2  7697  caofinvl  7708  fsplitfpar  8122  omxpenlem  9092  itunifn  10436  konigthlem  10587  seqof  14082  swrdlen  14670  mptfzshft  15799  prdsdsfn  17484  imasdsfn  17533  cidfn  17696  comffn  17722  isoval  17783  invf1o  17787  isofn  17793  brssc  17832  cofucl  17906  estrchomfn  18152  funcestrcsetclem4  18160  funcsetcestrclem4  18175  1stfcl  18214  2ndfcl  18215  prfcl  18220  evlfcl  18239  curf1cl  18245  curfcl  18249  hofcl  18276  yonedainv  18298  smndex1n0mnd  18895  grpinvf1o  18997  ghmquskerco  19272  pmtrrn  19443  pmtrfrn  19444  rnghmresfn  20584  rhmresfn  20613  rhmsubclem1  20650  srngf1o  20813  ofco2  22394  mat1dimscm  22418  neif  23043  fmf  23888  fncpn  25892  mdeg0  26032  om2noseqfo  28249  noseqrdglem  28256  noseqrdgfn  28257  noseqrdg0  28258  tglnfn  28531  grpoinvf  30518  kbass2  32103  fnresin  32609  f1o3d  32610  suppovss  32663  f1od2  32703  prodindf  32845  frlmdim  33656  pstmxmet  33933  ofcfn  34136  ofcfval2  34140  signstlen  34604  bnj941  34808  satfn  35382  msubrn  35556  poimirlem4  37653  cnambfre  37697  sdclem2  37771  diafn  41058  dibfna  41178  dicfnN  41207  dihf11lem  41290  mapd1o  41672  hdmapfnN  41853  hgmapfnN  41912  aks4d1p1p5  42093  hbtlem7  43116  fsovf1od  44007  ntrrn  44113  ntrf  44114  dssmapntrcls  44119  addrfn  44463  subrfn  44464  mulvfn  44465  fsumsermpt  45575  hoidmvlelem3  46593  smflimsuplem7  46822  rhmsubcALTVlem1  48223  funcringcsetcALTV2lem4  48235  funcringcsetclem4ALTV  48258  ackvalsucsucval  48635  sectfn  48966  invfn  48967  isofnALT  48968  iinfssclem2  48989  nelsubclem  49001  upeu4  49096  swapf2fn  49152  fucofn2  49202  fucofn22  49218