Theorem eqfnfvd 7025

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

Step	Hyp	Ref	Expression
1		eqfnfvd.3	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥))
2	1	ralrimiva 3154	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
3		eqfnfvd.1	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4		eqfnfvd.2	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴)
5		eqfnfv 7022	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
6	3, 4, 5	syl2anc 596	. 2 ⊢ (𝜑 → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
7	2, 6	mpbird 260	1 ⊢ (𝜑 → 𝐹 = 𝐺)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076   Fn wfn 6528  ‘cfv 6533

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-fv 6541

This theorem is used by:  foeqcnvco  7301  f1eqcocnv  7302  offveq  7704  tfrlem1  8364  updjudhcoinlf  9937  updjudhcoinrg  9938  ackbij2lem2  10241  ackbij2lem3  10242  fpwwe2lem7  10646  seqfeq2  14089  seqfeq  14091  seqfeq3  14116  ccatlid  14652  ccatrid  14653  ccatass  14654  ccatswrd  14738  swrdccat2  14739  pfxid  14754  ccatpfx  14770  pfxccat1  14771  swrdswrd  14774  cats1un  14790  swrdccatin1  14794  swrdccatin2  14798  pfxccatin12  14802  revccat  14835  revrev  14836  revpfxsfxrev  14837  cshco  14907  swrdco  14908  seqshft  15158  seq1st  16661  xpsfeq  17649  yonedainv  18369  mgmn0plusgplusf  18742  pwsco1mhm  18941  ghmquskerco  19411  f1otrspeq  19574  pmtrfinv  19588  symgtrinv  19599  frgpup3lem  19904  ablfac1eu  20202  zrinitorngc  20804  zrtermorngc  20805  zrtermoringc  20837  psgndiflemB  21813  frlmup1  22011  frlmup3  22013  frlmup4  22014  psrlidm  22176  psrridm  22177  psrass1  22178  subrgascl  22282  evlslem1  22298  evlsvvval  22309  psdmplcl  22390  psdvsca  22392  mavmulass  22771  upxp  23849  uptx  23851  cnextfres1  24294  ovolshftlem1  25737  volsup  25784  dvidlem  26142  dvrec  26182  dveq0  26227  dv11cn  26228  ftc1cn  26270  coemulc  26481  aannenlem1  26564  ulmuni  26628  ulmdv  26639  ostthlem1  27863  nvinvfval  31121  sspn  31217  kbass2  32598  xppreima2  33124  fdifsuppconst  33161  indpreima  33311  psgnfzto1stlem  33540  cycpmco2  33573  cyc3co2  33580  ply1gsumz  34009  mplasclco  34026  esplyind  34085  esumcvg  34596  signstres  35083  hgt750lemb  35164  subfacp1lem4  35762  cvmliftmolem2  35861  msubff1  36135  iprodefisumlem  36319  poimirlem8  38377  poimirlem13  38382  poimirlem14  38383  ftc1cnnc  38441  eqlkr3  39974  cdleme51finvN  41429  sticksstones11  43022  aks6d1c6lem4  43039  ofun  43105  frlmvscadiccat  43394  fiabv  43418  fsuppind  43436  ismrcd2  43544  ofoafo  44197  ofoaid1  44199  ofoaid2  44200  ofoaass  44201  ofoacom  44202  naddcnffo  44205  naddcnfcom  44207  naddcnfid1  44208  naddcnfass  44210  rfovcnvf1od  44844  dssmapntrcls  44968  dvconstbi  45158  fsumsermpt  46409  icccncfext  46715  voliooicof  46824  etransclem35  47097  rrxsnicc  47128  ovolval4lem1  47477  fcores  47955  1arymaptf1  49572  2arymaptf1  49583  tposideq  49814  fucoid  50274  prcofdiag1  50319  prcofdiag  50320  oppfdiag1  50340  oppfdiag  50342  funcsn  50467  crosspaltd  50799  crossp3d  50800  veronesevrowd  50812