Theorem fneq1d 6626

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-fun 6535  df-fn 6536

This theorem is used by:  fneq12d  6628  f1o00  6854  f1oprswap  6864  f1ompt  7105  fmpt2d  7119  f1ocnvd  7666  offn  7692  offval2f  7694  offval2  7699  ofrfval2  7700  caofinvl  7711  fsplitfpar  8116  omxpenlem  9079  itunifn  10422  konigthlem  10580  seqof  14126  swrdlen  14718  mptfzshft  15867  prdsdsfn  17553  imasdsfn  17603  cidfn  17770  comffn  17796  isoval  17857  invf1o  17861  isofn  17867  brssc  17906  cofucl  17980  estrchomfn  18226  funcestrcsetclem4  18234  funcsetcestrclem4  18249  1stfcl  18288  2ndfcl  18289  prfcl  18294  evlfcl  18313  curf1cl  18319  curfcl  18323  hofcl  18350  yonedainv  18372  smndex1n0mnd  19027  grpinvf1o  19135  ghmquskerco  19414  pmtrrn  19587  pmtrfrn  19588  rnghmresfn  20784  rhmresfn  20813  rhmsubclem1  20850  srngf1o  21017  ofco2  22676  mat1dimscm  22700  neif  23328  fmf  24174  fncpn  26163  mdeg0  26298  om2noseqfo  28566  noseqrdglem  28573  noseqrdgfn  28574  noseqrdg0  28575  tglnfn  28892  tgplnfn  29135  grpoinvf  31016  kbass2  32601  fnresin  33100  f1o3d  33102  suppovss  33156  f1od2  33193  prodindf  33311  esplyfval3  34085  frlmdim  34124  pstmxmet  34410  ofcfn  34613  ofcfval2  34617  signstlen  35078  bnj941  35285  satfn  35937  msubrn  36111  poimirlem4  38376  cnambfre  38420  sdclem2  38495  diafn  41910  dibfna  42030  dicfnN  42059  dihf11lem  42142  mapd1o  42524  hdmapfnN  42705  hgmapfnN  42764  aks4d1p1p5  42944  hbtlem7  43969  fsovf1od  44859  ntrrn  44965  ntrf  44966  dssmapntrcls  44971  addrfn  45297  subrfn  45298  mulvfn  45299  fsumsermpt  46412  hoidmvlelem3  47428  smflimsuplem7  47657  tmachlem-extpcover  47776  rhmsubcALTVlem1  49199  funcringcsetcALTV2lem4  49211  funcringcsetclem4ALTV  49234  ackvalsucsucval  49621  sectfn  49958  invfn  49959  isofnALT  49960  iinfssclem2  49984  nelsubclem  49996  upeu4  50125  swapf2fn  50197  fucofn2  50253  fucofn22  50269  fucoppc  50339  veronesevrowd  50815  veronesematrowd  50817