Theorem eqfnfv 7029

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

Step	Hyp	Ref	Expression
1		dffn5 6943	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6943	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2778	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 610	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6898	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3081	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 7013	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	bitrdi 290	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077  Vcvv 3451   ↦ cmpt 5186   Fn wfn 6533  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-fv 6546

This theorem is used by:  eqfnfv2  7030  eqfnfvd  7032  eqfnfv2f  7033  fsneq  7034  eqfnun  7036  fvreseq0  7037  fnmptfvd  7040  fndmdifeq0  7043  fneqeql  7045  fnnfpeq0  7183  fprb  7199  fconst2g  7209  cocan1  7299  cocan2  7300  weniso  7364  fsplitfpar  8129  fnsuppres  8208  tfr3  8407  ixpfi2  9339  fipreima  9347  updjud  10015  fseqenlem1  10103  fpwwe2lem7  10722  ofsubeq0  12317  ser0f  14198  hashgval2  14522  hashf1lem1  14600  prodf1f  16061  efcvgfsum  16252  prmreclem2  17095  1arithlem4  17104  1arith  17105  smndex1n0mnd  19111  isgrpinv  19204  dprdf11  20239  frlmplusgvalb  22075  frlmvscavalb  22076  islindf4  22144  psrbagconf1o  22237  pthaus  23957  xkohaus  23972  cnmpt11  23982  cnmpt21  23990  prdsxmetlem  24687  rrxmet  25729  rolle  26310  tdeglem4  26378  resinf1o  26864  dchrelbas2  27564  dchreq  27585  eqeefv  29481  axlowdimlem14  29533  elntg2  29563  nmlno0lem  31395  phoeqi  31459  occllem  31905  dfiop2  32355  hoeq  32362  ho01i  32430  hoeq1  32432  kbpj  32558  nmlnop0iALT  32597  lnopco0i  32606  nlelchi  32663  rnbra  32709  kbass5  32722  hmopidmchi  32753  hmopidmpji  32754  pjssdif2i  32776  pjinvari  32793  bnj1542  35487  bnj580  35543  subfacp1lem3  35947  subfacp1lem5  35949  mrsubff1  36279  msubff1  36321  faclimlem1  36508  rdgprc  36556  broucube  38572  cocanfo  38653  sdclem2  38676  rrnmet  38763  rrnequiv  38769  ltrnid  41192  ltrneq2  41205  tendoeq1  41821  sticksstones1  43196  pw2f1ocnv  44043  caofcan  45306  addrcom  45456  dvnprodlem1  46955  cfsetsnfsetf1  48128  cfsetsnfsetfo  48129  rrx2pnecoorneor  49826  rrx2linest  49853  dfinito4  50608