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

Theorem fneq1d 6159
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
StepHypRef Expression
1 fneq1d.1 . 2 (𝜑𝐹 = 𝐺)
2 fneq1 6157 . 2 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
31, 2syl 17 1 (𝜑 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1652   Fn wfn 6063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-br 4810  df-opab 4872  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-fun 6070  df-fn 6071
This theorem is referenced by:  fneq12d  6161  f1o00  6354  f1oprswap  6363  f1ompt  6571  fmpt2d  6583  f1ocnvd  7082  offn  7106  offval2f  7107  offval2  7112  ofrfval2  7113  caofinvl  7122  suppsnop  7511  omxpenlem  8268  itunifn  9492  konigthlem  9643  seqof  13065  swrdlen  13624  mptfzshft  14794  fprodrev  14990  prdsdsfn  16391  imasdsfn  16440  xpscfn  16485  cidfn  16605  comffn  16630  isoval  16690  invf1o  16694  isofn  16700  brssc  16739  cofucl  16813  estrchomfn  17040  funcestrcsetclem4  17049  funcsetcestrclem4  17064  1stfcl  17103  2ndfcl  17104  prfcl  17109  evlfcl  17128  curf1cl  17134  curfcl  17138  hofcl  17165  yonedainv  17187  grpinvf1o  17752  pmtrrn  18140  pmtrfrn  18141  srngf1o  19123  ofco2  20534  mat1dimscm  20558  neif  21184  fmf  22028  fncpn  23987  mdeg0  24121  tglnfn  25733  grpoinvf  27843  kbass2  29432  fnresin  29880  f1o3d  29881  f1od2  29948  pstmxmet  30387  prodindf  30532  ofcfn  30609  ofcfval2  30613  signstlen  31093  bnj941  31291  msubrn  31874  poimirlem4  33837  cnambfre  33881  sdclem2  33960  diafn  36990  dibfna  37110  dicfnN  37139  dihf11lem  37222  mapd1o  37604  hdmapfnN  37785  hgmapfnN  37844  hbtlem7  38372  fsovf1od  38984  ntrrn  39094  ntrf  39095  dssmapntrcls  39100  addrfn  39348  subrfn  39349  mulvfn  39350  fsumsermpt  40449  hoidmvlelem3  41451  smflimsuplem7  41672  rnghmresfn  42632  rhmresfn  42678  funcringcsetcALTV2lem4  42708  funcringcsetclem4ALTV  42731  rhmsubclem1  42755  rhmsubcALTVlem1  42773
  Copyright terms: Public domain W3C validator