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

Theorem eqfnfv 6102
Description: Equality of functions is determined by their values. Special case of Exercise 4 of [TakeutiZaring] p. 28 (with domain equality omitted). (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
Assertion
Ref Expression
eqfnfv ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐺

Proof of Theorem eqfnfv
StepHypRef Expression
1 dffn5 6034 . . 3 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
2 dffn5 6034 . . 3 (𝐺 Fn 𝐴𝐺 = (𝑥𝐴 ↦ (𝐺𝑥)))
3 eqeq12 2527 . . 3 ((𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) ∧ 𝐺 = (𝑥𝐴 ↦ (𝐺𝑥))) → (𝐹 = 𝐺 ↔ (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥))))
41, 2, 3syl2anb 494 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥))))
5 fvex 5996 . . . 4 (𝐹𝑥) ∈ V
65rgenw 2812 . . 3 𝑥𝐴 (𝐹𝑥) ∈ V
7 mpteqb 6090 . . 3 (∀𝑥𝐴 (𝐹𝑥) ∈ V → ((𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥)) ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
86, 7ax-mp 5 . 2 ((𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥)) ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥))
94, 8syl6bb 274 1 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1938  wral 2800  Vcvv 3077  cmpt 4541   Fn wfn 5684  cfv 5689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-mpt 4543  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-iota 5653  df-fun 5691  df-fn 5692  df-fv 5697
This theorem is referenced by:  eqfnfv2  6103  eqfnfvd  6105  eqfnfv2f  6106  fvreseq0  6108  fnmptfvd  6111  fndmdifeq0  6114  fneqeql  6116  fnnfpeq0  6225  fconst2g  6249  cocan1  6322  cocan2  6323  weniso  6380  fnsuppres  7083  tfr3  7257  ixpfi2  8022  fipreima  8030  fseqenlem1  8605  fpwwe2lem8  9213  ofsubeq0  10771  ser0f  12583  hashgval2  12892  hashf1lem1  12959  prodf1f  14330  efcvgfsum  14522  prmreclem2  15341  1arithlem4  15350  1arith  15351  isgrpinv  17185  dprdf11  18150  psrbagconf1o  19097  islindf4  19897  pthaus  21152  xkohaus  21167  cnmpt11  21177  cnmpt21  21185  prdsxmetlem  21883  rrxmet  22863  rolle  23433  tdeglem4  23500  resinf1o  23974  dchrelbas2  24652  dchreq  24673  eqeefv  25474  axlowdimlem14  25526  nmlno0lem  26811  phoeqi  26876  occllem  27335  dfiop2  27785  hoeq  27792  ho01i  27860  hoeq1  27862  kbpj  27988  nmlnop0iALT  28027  lnopco0i  28036  nlelchi  28093  rnbra  28139  kbass5  28152  hmopidmchi  28183  hmopidmpji  28184  pjssdif2i  28206  pjinvari  28223  bnj1542  30027  bnj580  30083  subfacp1lem3  30264  subfacp1lem5  30266  mrsubff1  30511  msubff1  30553  faclimlem1  30725  fprb  30759  rdgprc  30787  broucube  32488  cocanfo  32557  eqfnun  32561  sdclem2  32583  rrnmet  32673  rrnequiv  32679  ltrnid  34314  ltrneq2  34327  tendoeq1  34945  pw2f1ocnv  36497  caofcan  37426  addrcom  37582  fsneq  38277  dvnprodlem1  38726
  Copyright terms: Public domain W3C validator