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

Theorem eqfnfvd 6786
Description: Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.)
Hypotheses
Ref Expression
eqfnfvd.1 (𝜑𝐹 Fn 𝐴)
eqfnfvd.2 (𝜑𝐺 Fn 𝐴)
eqfnfvd.3 ((𝜑𝑥𝐴) → (𝐹𝑥) = (𝐺𝑥))
Assertion
Ref Expression
eqfnfvd (𝜑𝐹 = 𝐺)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐺   𝜑,𝑥

Proof of Theorem eqfnfvd
StepHypRef Expression
1 eqfnfvd.3 . . 3 ((𝜑𝑥𝐴) → (𝐹𝑥) = (𝐺𝑥))
21ralrimiva 3176 . 2 (𝜑 → ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥))
3 eqfnfvd.1 . . 3 (𝜑𝐹 Fn 𝐴)
4 eqfnfvd.2 . . 3 (𝜑𝐺 Fn 𝐴)
5 eqfnfv 6783 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
63, 4, 5syl2anc 587 . 2 (𝜑 → (𝐹 = 𝐺 ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
72, 6mpbird 260 1 (𝜑𝐹 = 𝐺)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wral 3132   Fn wfn 6331  cfv 6336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3137  df-rex 3138  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fn 6339  df-fv 6344
This theorem is referenced by:  foeqcnvco  7038  f1eqcocnv  7039  offveq  7413  tfrlem1  7995  updjudhcoinlf  9345  updjudhcoinrg  9346  ackbij2lem2  9647  ackbij2lem3  9648  fpwwe2lem8  10044  seqfeq2  13387  seqfeq  13389  seqfeq3  13414  ccatlid  13929  ccatrid  13930  ccatass  13931  ccatswrd  14019  swrdccat2  14020  pfxid  14035  ccatpfx  14052  pfxccat1  14053  swrdswrd  14056  cats1un  14072  swrdccatin1  14076  swrdccatin2  14080  pfxccatin12  14084  revccat  14117  revrev  14118  cshco  14187  swrdco  14188  seqshft  14433  seq1st  15902  xpsfeq  16825  yonedainv  17520  pwsco1mhm  17985  f1otrspeq  18564  pmtrfinv  18578  symgtrinv  18589  frgpup3lem  18892  ablfac1eu  19184  psrlidm  20169  psrridm  20170  psrass1  20171  subrgascl  20264  evlslem1  20281  psgndiflemB  20730  frlmup1  20928  frlmup3  20930  frlmup4  20931  mavmulass  21144  upxp  22217  uptx  22219  cnextfres1  22662  ovolshftlem1  24102  volsup  24149  dvidlem  24507  dvrec  24547  dveq0  24592  dv11cn  24593  ftc1cn  24635  coemulc  24841  aannenlem1  24913  ulmuni  24976  ulmdv  24987  ostthlem1  26200  nvinvfval  28412  sspn  28508  kbass2  29889  xppreima2  30392  psgnfzto1stlem  30760  cycpmco2  30793  cyc3co2  30800  indpreima  31302  esumcvg  31363  signstres  31863  hgt750lemb  31945  revpfxsfxrev  32380  subfacp1lem4  32448  cvmliftmolem2  32547  msubff1  32821  iprodefisumlem  32990  poimirlem8  34965  poimirlem13  34970  poimirlem14  34971  ftc1cnnc  35029  eqlkr3  36297  cdleme51finvN  37752  frlmvscadiccat  39296  ismrcd2  39472  rfovcnvf1od  40538  dssmapntrcls  40666  dvconstbi  40874  fsumsermpt  42063  icccncfext  42371  voliooicof  42480  etransclem35  42753  rrxsnicc  42784  ovolval4lem1  43130  zrinitorngc  44466  zrtermorngc  44467  zrtermoringc  44536  narymaptf1  44896
  Copyright terms: Public domain W3C validator