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

Theorem eqfnfvd 5800
Description: Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.)
Hypotheses
Ref Expression
eqfnfvd.1  |-  ( ph  ->  F  Fn  A )
eqfnfvd.2  |-  ( ph  ->  G  Fn  A )
eqfnfvd.3  |-  ( (
ph  /\  x  e.  A )  ->  ( F `  x )  =  ( G `  x ) )
Assertion
Ref Expression
eqfnfvd  |-  ( ph  ->  F  =  G )
Distinct variable groups:    x, A    x, F    x, G    ph, x

Proof of Theorem eqfnfvd
StepHypRef Expression
1 eqfnfvd.3 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  ( F `  x )  =  ( G `  x ) )
21ralrimiva 2799 . 2  |-  ( ph  ->  A. x  e.  A  ( F `  x )  =  ( G `  x ) )
3 eqfnfvd.1 . . 3  |-  ( ph  ->  F  Fn  A )
4 eqfnfvd.2 . . 3  |-  ( ph  ->  G  Fn  A )
5 eqfnfv 5797 . . 3  |-  ( ( F  Fn  A  /\  G  Fn  A )  ->  ( F  =  G  <->  A. x  e.  A  ( F `  x )  =  ( G `  x ) ) )
63, 4, 5syl2anc 661 . 2  |-  ( ph  ->  ( F  =  G  <->  A. x  e.  A  ( F `  x )  =  ( G `  x ) ) )
72, 6mpbird 232 1  |-  ( ph  ->  F  =  G )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2715    Fn wfn 5413   ` cfv 5418
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-fv 5426
This theorem is referenced by:  foeqcnvco  5998  f1eqcocnv  5999  offveq  6341  tfrlem1  6835  ackbij2lem2  8409  ackbij2lem3  8410  fpwwe2lem8  8804  seqfeq2  11829  seqfeq  11831  seqfeq3  11856  ccatlid  12284  ccatrid  12285  ccatass  12286  eqs1  12300  swrdid  12321  ccatswrd  12350  swrdccat1  12351  swrdccat2  12352  swrdswrd  12354  cats1un  12370  swrdccatin1  12374  swrdccatin2  12378  swrdccatin12  12382  revccat  12406  revrev  12407  cshco  12464  swrdco  12465  seqshft  12574  seq1st  13746  xpsfeq  14502  yonedainv  15091  pwsco1mhm  15498  f1otrspeq  15953  pmtrfinv  15967  symgtrinv  15978  frgpup3lem  16274  ablfac1eu  16574  psrlidm  17474  psrlidmOLD  17475  psrridm  17476  psrridmOLD  17477  psrass1  17478  subrgascl  17580  evlslem1  17601  psgndiflemB  18030  frlmup1  18226  frlmup3  18228  frlmup4  18229  mavmulass  18360  upxp  19196  uptx  19198  cnextfres  19640  ovolshftlem1  20992  volsup  21037  dvidlem  21390  dvrec  21429  dveq0  21472  dv11cn  21473  ftc1cn  21515  coemulc  21722  aannenlem1  21794  ulmuni  21857  ulmdv  21868  ostthlem1  22876  nvinvfval  24020  sspn  24134  kbass2  25521  xppreima2  25965  indpreima  26481  esumcvg  26535  subfacp1lem4  27071  cvmliftmolem2  27171  iprodefisumlem  27504  ftc1cnnc  28466  ismrcd2  29035  dvconstbi  29608  eqlkr3  32746  cdleme51finvN  34200
  Copyright terms: Public domain W3C validator