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

Theorem fneq1d 5941
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 5939 . 2 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
31, 2syl 17 1 (𝜑 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480   Fn wfn 5845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-br 4619  df-opab 4679  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-fun 5852  df-fn 5853
This theorem is referenced by:  fneq12d  5943  f1o00  6130  f1oprswap  6139  f1ompt  6339  fmpt2d  6349  f1ocnvd  6838  offn  6862  offval2f  6863  offval2  6868  ofrfval2  6869  caofinvl  6878  suppsnop  7255  omxpenlem  8006  itunifn  9184  konigthlem  9335  seqof  12795  swrdlen  13356  mptfzshft  14433  fsumrev  14434  fprodrev  14627  prdsdsfn  16041  imasdsfn  16090  xpscfn  16135  cidfn  16256  comffn  16281  isoval  16341  invf1o  16345  isofn  16351  brssc  16390  cofucl  16464  estrchomfn  16691  funcestrcsetclem4  16699  funcsetcestrclem4  16714  1stfcl  16753  2ndfcl  16754  prfcl  16759  evlfcl  16778  curf1cl  16784  curfcl  16788  hofcl  16815  yonedainv  16837  grpinvf1o  17401  pmtrrn  17793  pmtrfrn  17794  srngf1o  18770  ofco2  20171  mat1dimscm  20195  neif  20809  fmf  21654  fncpn  23597  mdeg0  23729  tglnfn  25337  grpoinvf  27226  kbass2  28816  fnresin  29265  f1o3d  29266  f1od2  29333  pstmxmet  29714  ofcfn  29935  ofcfval2  29939  signstlen  30416  bnj941  30543  msubrn  31126  poimirlem4  33031  cnambfre  33076  sdclem2  33156  diafn  35789  dibfna  35909  dicfnN  35938  dihf11lem  36021  mapd1o  36403  hdmapfnN  36587  hgmapfnN  36646  hbtlem7  37162  fsovf1od  37778  ntrrn  37888  ntrf  37889  dssmapntrcls  37894  addrfn  38144  subrfn  38145  mulvfn  38146  fsumsermpt  39202  hoidmvlelem3  40105  smflimsuplem7  40326  rnghmresfn  41224  rhmresfn  41270  funcringcsetcALTV2lem4  41300  funcringcsetclem4ALTV  41323  rhmsubclem1  41347  rhmsubcALTVlem1  41365
  Copyright terms: Public domain W3C validator