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

Theorem fneq1i 5680
Description: Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
fneq1i.1
Assertion
Ref Expression
fneq1i

Proof of Theorem fneq1i
StepHypRef Expression
1 fneq1i.1 . 2
2 fneq1 5674 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395  Fnwfn 5588
This theorem is referenced by:  fnunsn  5693  fnopabg  5709  f1oun  5840  f1oi  5856  f1osn  5858  ovid  6419  curry1  6892  curry2  6895  tfrlem10  7075  tfr1  7085  seqomlem2  7135  seqomlem3  7136  seqomlem4  7137  fnseqom  7139  unblem4  7795  r1fnon  8206  alephfnon  8467  alephfplem4  8509  alephfp  8510  cfsmolem  8671  infpssrlem3  8706  compssiso  8775  hsmexlem5  8831  axdclem2  8921  wunex2  9137  wuncval2  9146  om2uzrani  12063  om2uzf1oi  12064  uzrdglem  12068  uzrdgfni  12069  uzrdg0i  12070  hashkf  12407  dmaf  15376  cdaf  15377  prdsinvlem  16178  srg1zr  17180  pws1  17265  frlmphl  18812  ovolunlem1  21908  0plef  22079  0pledm  22080  itg1ge0  22093  itg1addlem4  22106  mbfi1fseqlem5  22126  itg2addlem  22165  qaa  22719  2trllemD  24559  eupap1  24976  ghgrpOLD  25370  0vfval  25499  mptfnf  27499  xrge0pluscn  27922  wfrlem5  29347  wfrlem13  29355  frrlem5  29391  fullfunfnv  29596  neibastop2lem  30178  fourierdlem42  31931  rngcrescrhm  32893  rngcrescrhmOLD  32912  bnj927  33827  bnj535  33948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-fun 5595  df-fn 5596
  Copyright terms: Public domain W3C validator