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

Theorem fneq1d 5662
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 5660 . 2  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )
31, 2syl 16 1  |-  ( ph  ->  ( F  Fn  A  <->  G  Fn  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1374    Fn wfn 5574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-opab 4499  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-fun 5581  df-fn 5582
This theorem is referenced by:  fneq12d  5664  f1o00  5839  f1oprswap  5846  f1ompt  6034  fmpt2d  6042  f1ocnvd  6499  offn  6526  offval2  6531  ofrfval2  6532  caofinvl  6542  suppsnop  6905  omxpenlem  7608  itunifn  8786  konigthlem  8932  seqof  12120  swrdlen  12600  mptfzshft  13542  fsumrev  13543  prdsdsfn  14709  imasdsfn  14758  xpscfn  14803  cidfn  14923  comffn  14950  isoval  15009  invf1o  15013  brssc  15033  cofucl  15104  1stfcl  15313  2ndfcl  15314  prfcl  15319  evlfcl  15338  curf1cl  15344  curfcl  15348  hofcl  15375  yonedainv  15397  grpinvf1o  15902  pmtrrn  16271  pmtrfrn  16272  srngf1o  17279  ofco2  18713  mat1dimscm  18737  neif  19360  fmf  20174  fncpn  22064  mdeg0  22198  tglnfn  23655  grpoinvf  24768  kbass2  26562  fnresin  26993  f1o3d  26994  offval2f  27028  f1od2  27069  pstmxmet  27362  ofcfn  27589  ofcfval2  27593  signstlen  28014  fprodshft  28533  fprodrev  28534  cnambfre  29491  sdclem2  29689  hbtlem7  30531  addrfn  30778  subrfn  30779  mulvfn  30780  bnj941  32785  diafn  35706  dibfna  35826  dicfnN  35855  dihf11lem  35938  mapd1o  36320  hdmapfnN  36504  hgmapfnN  36563
  Copyright terms: Public domain W3C validator