Theorem fneq1d 6432

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   Fn wfn 6335

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-br 5037  df-opab 5099  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-fun 6342  df-fn 6343

This theorem is referenced by:  fneq12d  6434  f1o00  6641  f1oprswap  6650  f1ompt  6872  fmpt2d  6884  f1ocnvd  7398  offn  7423  offval2f  7425  offval2  7430  ofrfval2  7431  caofinvl  7440  fsplitfpar  7825  omxpenlem  8652  itunifn  9890  konigthlem  10041  seqof  13490  swrdlen  14069  mptfzshft  15194  prdsdsfn  16809  imasdsfn  16858  cidfn  17021  comffn  17046  isoval  17107  invf1o  17111  isofn  17117  brssc  17156  cofucl  17230  estrchomfn  17464  funcestrcsetclem4  17472  funcsetcestrclem4  17487  1stfcl  17526  2ndfcl  17527  prfcl  17532  evlfcl  17551  curf1cl  17557  curfcl  17561  hofcl  17588  yonedainv  17610  smndex1n0mnd  18156  grpinvf1o  18249  pmtrrn  18665  pmtrfrn  18666  srngf1o  19706  ofco2  21164  mat1dimscm  21188  neif  21813  fmf  22658  fncpn  24645  mdeg0  24783  tglnfn  26453  grpoinvf  28427  kbass2  30012  fnresin  30496  f1o3d  30497  suppovss  30553  f1od2  30592  frlmdim  31227  pstmxmet  31380  prodindf  31522  ofcfn  31599  ofcfval2  31603  signstlen  32077  bnj941  32284  satfn  32845  msubrn  33019  poimirlem4  35375  cnambfre  35419  sdclem2  35494  diafn  38644  dibfna  38764  dicfnN  38793  dihf11lem  38876  mapd1o  39258  hdmapfnN  39439  hgmapfnN  39498  aks4d1p1p5  39675  hbtlem7  40477  fsovf1od  41125  ntrrn  41233  ntrf  41234  dssmapntrcls  41239  addrfn  41584  subrfn  41585  mulvfn  41586  fsumsermpt  42622  hoidmvlelem3  43637  smflimsuplem7  43858  rnghmresfn  45003  rhmresfn  45049  funcringcsetcALTV2lem4  45079  funcringcsetclem4ALTV  45102  rhmsubclem1  45126  rhmsubcALTVlem1  45144  ackvalsucsucval  45516