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

Theorem fneq1d 5652
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 5650 . 2  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )
31, 2syl 17 1  |-  ( ph  ->  ( F  Fn  A  <->  G  Fn  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1405    Fn wfn 5564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-br 4396  df-opab 4454  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-fun 5571  df-fn 5572
This theorem is referenced by:  fneq12d  5654  f1o00  5831  f1oprswap  5838  f1ompt  6031  fmpt2d  6040  f1ocnvd  6505  offn  6532  offval2f  6533  offval2  6538  ofrfval2  6539  caofinvl  6549  suppsnop  6916  omxpenlem  7656  itunifn  8829  konigthlem  8975  seqof  12208  swrdlen  12704  mptfzshft  13744  fsumrev  13745  fprodrev  13933  prdsdsfn  15079  imasdsfn  15128  xpscfn  15173  cidfn  15293  comffn  15318  isoval  15378  invf1o  15382  isofn  15388  brssc  15427  cofucl  15501  estrchomfn  15728  funcestrcsetclem4  15736  funcsetcestrclem4  15751  1stfcl  15790  2ndfcl  15791  prfcl  15796  evlfcl  15815  curf1cl  15821  curfcl  15825  hofcl  15852  yonedainv  15874  grpinvf1o  16432  pmtrrn  16806  pmtrfrn  16807  srngf1o  17823  ofco2  19245  mat1dimscm  19269  neif  19894  fmf  20738  fncpn  22628  mdeg0  22762  tglnfn  24317  grpoinvf  25656  kbass2  27449  fnresin  27911  f1o3d  27912  f1od2  27994  pstmxmet  28329  ofcfn  28547  ofcfval2  28551  signstlen  29030  bnj941  29158  msubrn  29741  cnambfre  31435  sdclem2  31517  diafn  34054  dibfna  34174  dicfnN  34203  dihf11lem  34286  mapd1o  34668  hdmapfnN  34852  hgmapfnN  34911  hbtlem7  35438  addrfn  36229  subrfn  36230  mulvfn  36231  rnghmresfn  38282  rhmresfn  38328  funcringcsetcALTV2lem4  38358  funcringcsetclem4ALTV  38381  rhmsubclem1  38405  rhmsubcALTVlem1  38424
  Copyright terms: Public domain W3C validator