Theorem fneq1d 6593

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   Fn wfn 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-fun 6502  df-fn 6503

This theorem is referenced by:  fneq12d  6595  f1o00  6817  f1oprswap  6827  f1ompt  7065  fmpt2d  7079  f1ocnvd  7619  offn  7645  offval2f  7647  offval2  7652  ofrfval2  7653  caofinvl  7664  fsplitfpar  8070  omxpenlem  9018  itunifn  10339  konigthlem  10491  seqof  13994  swrdlen  14583  mptfzshft  15713  prdsdsfn  17397  imasdsfn  17447  cidfn  17614  comffn  17640  isoval  17701  invf1o  17705  isofn  17711  brssc  17750  cofucl  17824  estrchomfn  18070  funcestrcsetclem4  18078  funcsetcestrclem4  18093  1stfcl  18132  2ndfcl  18133  prfcl  18138  evlfcl  18157  curf1cl  18163  curfcl  18167  hofcl  18194  yonedainv  18216  smndex1n0mnd  18849  grpinvf1o  18951  ghmquskerco  19225  pmtrrn  19398  pmtrfrn  19399  rnghmresfn  20564  rhmresfn  20593  rhmsubclem1  20630  srngf1o  20793  ofco2  22407  mat1dimscm  22431  neif  23056  fmf  23901  fncpn  25903  mdeg0  26043  om2noseqfo  28306  noseqrdglem  28313  noseqrdgfn  28314  noseqrdg0  28315  tglnfn  28631  grpoinvf  30619  kbass2  32204  fnresin  32713  f1o3d  32715  suppovss  32770  f1od2  32808  prodindf  32954  esplyfval3  33748  frlmdim  33788  pstmxmet  34074  ofcfn  34277  ofcfval2  34281  signstlen  34744  bnj941  34948  satfn  35568  msubrn  35742  poimirlem4  37869  cnambfre  37913  sdclem2  37987  diafn  41404  dibfna  41524  dicfnN  41553  dihf11lem  41636  mapd1o  42018  hdmapfnN  42199  hgmapfnN  42258  aks4d1p1p5  42439  hbtlem7  43476  fsovf1od  44366  ntrrn  44472  ntrf  44473  dssmapntrcls  44478  addrfn  44821  subrfn  44822  mulvfn  44823  fsumsermpt  45933  hoidmvlelem3  46949  smflimsuplem7  47178  rhmsubcALTVlem1  48635  funcringcsetcALTV2lem4  48647  funcringcsetclem4ALTV  48670  ackvalsucsucval  49042  sectfn  49382  invfn  49383  isofnALT  49384  iinfssclem2  49408  nelsubclem  49420  upeu4  49549  swapf2fn  49621  fucofn2  49677  fucofn22  49693  fucoppc  49763