Theorem eqfnfvd 7026

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 3163	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
3		eqfnfvd.1	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4		eqfnfvd.2	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴)
5		eqfnfv 7023	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
6	3, 4, 5	syl2anc 595	. 2 ⊢ (𝜑 → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
7	2, 6	mpbird 260	1 ⊢ (𝜑 → 𝐹 = 𝐺)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085   Fn wfn 6529  ‘cfv 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6490  df-fun 6536  df-fn 6537  df-fv 6542

This theorem is referenced by:  foeqcnvco  7296  f1eqcocnv  7297  offveq  7698  tfrlem1  8358  updjudhcoinlf  9914  updjudhcoinrg  9915  ackbij2lem2  10218  ackbij2lem3  10219  fpwwe2lem7  10618  seqfeq2  14057  seqfeq  14059  seqfeq3  14084  ccatlid  14620  ccatrid  14621  ccatass  14622  ccatswrd  14702  swrdccat2  14703  pfxid  14718  ccatpfx  14734  pfxccat1  14735  swrdswrd  14738  cats1un  14754  swrdccatin1  14758  swrdccatin2  14762  pfxccatin12  14766  revccat  14799  revrev  14800  cshco  14869  swrdco  14870  seqshft  15118  seq1st  16625  xpsfeq  17613  yonedainv  18333  pwsco1mhm  18887  ghmquskerco  19350  f1otrspeq  19513  pmtrfinv  19527  symgtrinv  19538  frgpup3lem  19843  ablfac1eu  20141  zrinitorngc  20723  zrtermorngc  20724  zrtermoringc  20756  psgndiflemB  21715  frlmup1  21913  frlmup3  21915  frlmup4  21916  psrlidm  22076  psrridm  22077  psrass1  22078  subrgascl  22182  evlslem1  22198  evlsvvval  22209  psdmplcl  22290  psdvsca  22292  mavmulass  22671  upxp  23745  uptx  23747  cnextfres1  24190  ovolshftlem1  25633  volsup  25680  dvidlem  26039  dvrec  26079  dveq0  26124  dv11cn  26125  ftc1cn  26167  coemulc  26377  aannenlem1  26454  ulmuni  26517  ulmdv  26528  ostthlem1  27753  nvinvfval  30929  sspn  31025  kbass2  32406  xppreima2  32933  fdifsuppconst  32971  indpreima  33122  psgnfzto1stlem  33357  cycpmco2  33390  cyc3co2  33397  ply1gsumz  33830  mplasclco  33847  esplyind  33906  esumcvg  34417  signstres  34903  hgt750lemb  34984  revpfxsfxrev  35502  subfacp1lem4  35570  cvmliftmolem2  35669  msubff1  35943  iprodefisumlem  36127  poimirlem8  38162  poimirlem13  38167  poimirlem14  38168  ftc1cnnc  38226  eqlkr3  39760  cdleme51finvN  41215  sticksstones11  42808  aks6d1c6lem4  42825  ofun  42891  frlmvscadiccat  43165  fiabv  43191  fsuppind  43209  ismrcd2  43317  ofoafo  43970  ofoaid1  43972  ofoaid2  43973  ofoaass  43974  ofoacom  43975  naddcnffo  43978  naddcnfcom  43980  naddcnfid1  43981  naddcnfass  43983  rfovcnvf1od  44617  dssmapntrcls  44741  dvconstbi  44931  fsumsermpt  46182  icccncfext  46488  voliooicof  46597  etransclem35  46870  rrxsnicc  46901  ovolval4lem1  47250  fcores  47688  1arymaptf1  49302  2arymaptf1  49313  tposideq  49546  fucoid  50006  prcofdiag1  50051  prcofdiag  50052  oppfdiag1  50072  oppfdiag  50074  funcsn  50199