MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fneq1d Structured version   Unicode version

Theorem fneq1d 5539
Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
fneq1d.1  |-  ( ph  ->  F  =  G )
Assertion
Ref Expression
fneq1d  |-  ( ph  ->  ( F  Fn  A  <->  G  Fn  A ) )

Proof of Theorem fneq1d
StepHypRef Expression
1 fneq1d.1 . 2  |-  ( ph  ->  F  =  G )
2 fneq1 5537 . 2  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )
31, 2syl 16 1  |-  ( ph  ->  ( F  Fn  A  <->  G  Fn  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653    Fn wfn 5452
This theorem is referenced by:  fneq12d  5541  f1o00  5713  f1oprswap  5720  f1ompt  5894  fmpt2d  5901  f1ocnvd  6296  offn  6319  offval2  6325  ofrfval2  6326  caofinvl  6334  omxpenlem  7212  itunifn  8302  konigthlem  8448  seqof  11385  swrdlen  11775  fsumrev  12567  fsumshft  12568  prdsdsfn  13692  imasdsfn  13745  xpscfn  13789  cidfn  13909  comffn  13936  isoval  13995  invf1o  13999  brssc  14019  cofucl  14090  1stfcl  14299  2ndfcl  14300  prfcl  14305  evlfcl  14324  curf1cl  14330  curfcl  14334  hofcl  14361  yonedainv  14383  grpinvf1o  14866  srngf1o  15947  neif  17169  fmf  17982  fncpn  19824  grpoinvf  21833  kbass2  23625  f1o3d  24046  offval2f  24085  pstmxmet  24297  ofcfn  24488  ofcfval2  24492  fprodshft  25305  fprodrev  25306  cnambfre  26267  sdclem2  26460  hbtlem7  27320  pmtrrn  27390  pmtrfrn  27391  addrfn  27667  subrfn  27668  mulvfn  27669  bnj941  29217  diafn  31906  dibfna  32026  dicfnN  32055  dihf11lem  32138  mapd1o  32520  hdmapfnN  32704  hgmapfnN  32763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216  df-opab 4270  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-fun 5459  df-fn 5460
  Copyright terms: Public domain W3C validator