Theorem fneq1d 6579

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-fun 6488  df-fn 6489

This theorem is referenced by:  fneq12d  6581  f1o00  6803  f1oprswap  6812  f1ompt  7049  fmpt2d  7062  f1ocnvd  7604  offn  7630  offval2f  7632  offval2  7637  ofrfval2  7638  caofinvl  7649  fsplitfpar  8058  omxpenlem  9002  itunifn  10330  konigthlem  10481  seqof  13984  swrdlen  14572  mptfzshft  15703  prdsdsfn  17387  imasdsfn  17436  cidfn  17603  comffn  17629  isoval  17690  invf1o  17694  isofn  17700  brssc  17739  cofucl  17813  estrchomfn  18059  funcestrcsetclem4  18067  funcsetcestrclem4  18082  1stfcl  18121  2ndfcl  18122  prfcl  18127  evlfcl  18146  curf1cl  18152  curfcl  18156  hofcl  18183  yonedainv  18205  smndex1n0mnd  18804  grpinvf1o  18906  ghmquskerco  19181  pmtrrn  19354  pmtrfrn  19355  rnghmresfn  20522  rhmresfn  20551  rhmsubclem1  20588  srngf1o  20751  ofco2  22354  mat1dimscm  22378  neif  23003  fmf  23848  fncpn  25851  mdeg0  25991  om2noseqfo  28215  noseqrdglem  28222  noseqrdgfn  28223  noseqrdg0  28224  tglnfn  28510  grpoinvf  30494  kbass2  32079  fnresin  32583  f1o3d  32584  suppovss  32637  f1od2  32677  prodindf  32819  frlmdim  33583  pstmxmet  33863  ofcfn  34066  ofcfval2  34070  signstlen  34534  bnj941  34738  satfn  35327  msubrn  35501  poimirlem4  37603  cnambfre  37647  sdclem2  37721  diafn  41013  dibfna  41133  dicfnN  41162  dihf11lem  41245  mapd1o  41627  hdmapfnN  41808  hgmapfnN  41867  aks4d1p1p5  42048  hbtlem7  43098  fsovf1od  43989  ntrrn  44095  ntrf  44096  dssmapntrcls  44101  addrfn  44445  subrfn  44446  mulvfn  44447  fsumsermpt  45561  hoidmvlelem3  46579  smflimsuplem7  46808  rhmsubcALTVlem1  48266  funcringcsetcALTV2lem4  48278  funcringcsetclem4ALTV  48301  ackvalsucsucval  48674  sectfn  49015  invfn  49016  isofnALT  49017  iinfssclem2  49041  nelsubclem  49053  upeu4  49182  swapf2fn  49254  fucofn2  49310  fucofn22  49326  fucoppc  49396