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

Theorem eqfnfvd 5984
Description: Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.)
Hypotheses
Ref Expression
eqfnfvd.1
eqfnfvd.2
eqfnfvd.3
Assertion
Ref Expression
eqfnfvd
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem eqfnfvd
StepHypRef Expression
1 eqfnfvd.3 . . 3
21ralrimiva 2871 . 2
3 eqfnfvd.1 . . 3
4 eqfnfvd.2 . . 3
5 eqfnfv 5981 . . 3
63, 4, 5syl2anc 661 . 2
72, 6mpbird 232 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807  Fnwfn 5588  `cfv 5593
This theorem is referenced by:  foeqcnvco  6203  f1eqcocnv  6204  offveq  6561  tfrlem1  7064  ackbij2lem2  8641  ackbij2lem3  8642  fpwwe2lem8  9036  seqfeq2  12130  seqfeq  12132  seqfeq3  12157  ccatlid  12603  ccatrid  12604  ccatass  12605  eqs1  12621  swrdid  12652  ccatswrd  12681  swrdccat1  12682  swrdccat2  12683  swrdswrd  12685  cats1un  12701  swrdccatin1  12708  swrdccatin2  12712  swrdccatin12  12716  revccat  12740  revrev  12741  cshco  12802  swrdco  12803  seqshft  12918  seq1st  14200  xpsfeq  14961  yonedainv  15550  pwsco1mhm  16001  f1otrspeq  16472  pmtrfinv  16486  symgtrinv  16497  frgpup3lem  16795  ablfac1eu  17124  psrlidm  18056  psrlidmOLD  18057  psrridm  18058  psrridmOLD  18059  psrass1  18060  subrgascl  18163  evlslem1  18184  psgndiflemB  18636  frlmup1  18832  frlmup3  18834  frlmup4  18835  mavmulass  19051  upxp  20124  uptx  20126  cnextfres  20568  ovolshftlem1  21920  volsup  21966  dvidlem  22319  dvrec  22358  dveq0  22401  dv11cn  22402  ftc1cn  22444  coemulc  22652  aannenlem1  22724  ulmuni  22787  ulmdv  22798  ostthlem1  23812  nvinvfval  25535  sspn  25649  kbass2  27036  xppreima2  27488  indpreima  28038  esumcvg  28092  signstres  28532  subfacp1lem4  28627  cvmliftmolem2  28727  msubff1  28916  iprodefisumlem  29123  ftc1cnnc  30089  ismrcd2  30631  dvconstbi  31239  icccncfext  31690  etransclem35  32052  zrinitorngc  32808  zrtermorngc  32809  zrtermoringc  32878  eqlkr3  34826  cdleme51finvN  36282
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-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691
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-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  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-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-fv 5601
  Copyright terms: Public domain W3C validator