Theorem fneq1d 6574

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   Fn wfn 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-fun 6483  df-fn 6484

This theorem is referenced by:  fneq12d  6576  f1o00  6798  f1oprswap  6807  f1ompt  7044  fmpt2d  7057  f1ocnvd  7597  offn  7623  offval2f  7625  offval2  7630  ofrfval2  7631  caofinvl  7642  fsplitfpar  8048  omxpenlem  8991  itunifn  10305  konigthlem  10456  seqof  13963  swrdlen  14552  mptfzshft  15682  prdsdsfn  17366  imasdsfn  17415  cidfn  17582  comffn  17608  isoval  17669  invf1o  17673  isofn  17679  brssc  17718  cofucl  17792  estrchomfn  18038  funcestrcsetclem4  18046  funcsetcestrclem4  18061  1stfcl  18100  2ndfcl  18101  prfcl  18106  evlfcl  18125  curf1cl  18131  curfcl  18135  hofcl  18162  yonedainv  18184  smndex1n0mnd  18817  grpinvf1o  18919  ghmquskerco  19194  pmtrrn  19367  pmtrfrn  19368  rnghmresfn  20532  rhmresfn  20561  rhmsubclem1  20598  srngf1o  20761  ofco2  22364  mat1dimscm  22388  neif  23013  fmf  23858  fncpn  25860  mdeg0  26000  om2noseqfo  28226  noseqrdglem  28233  noseqrdgfn  28234  noseqrdg0  28235  tglnfn  28523  grpoinvf  30507  kbass2  32092  fnresin  32602  f1o3d  32603  suppovss  32657  f1od2  32697  prodindf  32839  frlmdim  33619  pstmxmet  33905  ofcfn  34108  ofcfval2  34112  signstlen  34575  bnj941  34779  satfn  35387  msubrn  35561  poimirlem4  37663  cnambfre  37707  sdclem2  37781  diafn  41072  dibfna  41192  dicfnN  41221  dihf11lem  41304  mapd1o  41686  hdmapfnN  41867  hgmapfnN  41926  aks4d1p1p5  42107  hbtlem7  43157  fsovf1od  44048  ntrrn  44154  ntrf  44155  dssmapntrcls  44160  addrfn  44503  subrfn  44504  mulvfn  44505  fsumsermpt  45618  hoidmvlelem3  46634  smflimsuplem7  46863  rhmsubcALTVlem1  48311  funcringcsetcALTV2lem4  48323  funcringcsetclem4ALTV  48346  ackvalsucsucval  48719  sectfn  49060  invfn  49061  isofnALT  49062  iinfssclem2  49086  nelsubclem  49098  upeu4  49227  swapf2fn  49299  fucofn2  49355  fucofn22  49371  fucoppc  49441