Theorem eqfnfvd 6979

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3051   Fn wfn 6487  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500

This theorem is referenced by:  foeqcnvco  7246  f1eqcocnv  7247  offveq  7648  tfrlem1  8307  updjudhcoinlf  9844  updjudhcoinrg  9845  ackbij2lem2  10149  ackbij2lem3  10150  fpwwe2lem7  10548  seqfeq2  13948  seqfeq  13950  seqfeq3  13975  ccatlid  14510  ccatrid  14511  ccatass  14512  ccatswrd  14592  swrdccat2  14593  pfxid  14608  ccatpfx  14624  pfxccat1  14625  swrdswrd  14628  cats1un  14644  swrdccatin1  14648  swrdccatin2  14652  pfxccatin12  14656  revccat  14689  revrev  14690  cshco  14759  swrdco  14760  seqshft  15008  seq1st  16498  xpsfeq  17484  yonedainv  18204  pwsco1mhm  18757  ghmquskerco  19213  f1otrspeq  19376  pmtrfinv  19390  symgtrinv  19401  frgpup3lem  19706  ablfac1eu  20004  zrinitorngc  20575  zrtermorngc  20576  zrtermoringc  20608  psgndiflemB  21555  frlmup1  21753  frlmup3  21755  frlmup4  21756  psrlidm  21917  psrridm  21918  psrass1  21919  subrgascl  22021  evlslem1  22037  evlsvvval  22048  psdmplcl  22105  psdvsca  22107  mavmulass  22493  upxp  23567  uptx  23569  cnextfres1  24012  ovolshftlem1  25466  volsup  25513  dvidlem  25872  dvrec  25915  dveq0  25961  dv11cn  25962  ftc1cn  26006  coemulc  26216  aannenlem1  26292  ulmuni  26357  ulmdv  26368  ostthlem1  27594  nvinvfval  30715  sspn  30811  kbass2  32192  xppreima2  32729  fdifsuppconst  32768  indpreima  32947  psgnfzto1stlem  33182  cycpmco2  33215  cyc3co2  33222  ply1gsumz  33680  esplyind  33731  esumcvg  34243  signstres  34732  hgt750lemb  34813  revpfxsfxrev  35310  subfacp1lem4  35377  cvmliftmolem2  35476  msubff1  35750  iprodefisumlem  35934  poimirlem8  37829  poimirlem13  37834  poimirlem14  37835  ftc1cnnc  37893  eqlkr3  39361  cdleme51finvN  40816  sticksstones11  42410  aks6d1c6lem4  42427  ofun  42492  frlmvscadiccat  42761  fiabv  42791  fsuppind  42833  ismrcd2  42941  ofoafo  43598  ofoaid1  43600  ofoaid2  43601  ofoaass  43602  ofoacom  43603  naddcnffo  43606  naddcnfcom  43608  naddcnfid1  43609  naddcnfass  43611  rfovcnvf1od  44245  dssmapntrcls  44369  dvconstbi  44575  fsumsermpt  45825  icccncfext  46131  voliooicof  46240  etransclem35  46513  rrxsnicc  46544  ovolval4lem1  46893  fcores  47313  1arymaptf1  48888  2arymaptf1  48899  tposideq  49133  fucoid  49593  prcofdiag1  49638  prcofdiag  49639  oppfdiag1  49659  oppfdiag  49661  funcsn  49786