Theorem eqfnfvd 7035

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3061   Fn wfn 6538  ‘cfv 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-fv 6551

This theorem is referenced by:  foeqcnvco  7300  f1eqcocnv  7301  f1eqcocnvOLD  7302  offveq  7696  tfrlem1  8378  updjudhcoinlf  9929  updjudhcoinrg  9930  ackbij2lem2  10237  ackbij2lem3  10238  fpwwe2lem7  10634  seqfeq2  13995  seqfeq  13997  seqfeq3  14022  ccatlid  14540  ccatrid  14541  ccatass  14542  ccatswrd  14622  swrdccat2  14623  pfxid  14638  ccatpfx  14655  pfxccat1  14656  swrdswrd  14659  cats1un  14675  swrdccatin1  14679  swrdccatin2  14683  pfxccatin12  14687  revccat  14720  revrev  14721  cshco  14791  swrdco  14792  seqshft  15036  seq1st  16512  xpsfeq  17513  yonedainv  18238  pwsco1mhm  18749  f1otrspeq  19356  pmtrfinv  19370  symgtrinv  19381  frgpup3lem  19686  ablfac1eu  19984  psgndiflemB  21372  frlmup1  21572  frlmup3  21574  frlmup4  21575  psrlidm  21742  psrridm  21743  psrass1  21744  subrgascl  21846  evlslem1  21864  mavmulass  22271  upxp  23347  uptx  23349  cnextfres1  23792  ovolshftlem1  25250  volsup  25297  dvidlem  25656  dvrec  25696  dveq0  25741  dv11cn  25742  ftc1cn  25784  coemulc  25993  aannenlem1  26065  ulmuni  26128  ulmdv  26139  ostthlem1  27354  nvinvfval  30148  sspn  30244  kbass2  31625  xppreima2  32131  fdifsuppconst  32166  psgnfzto1stlem  32517  cycpmco2  32550  cyc3co2  32557  ghmquskerco  32791  ply1gsumz  32932  indpreima  33309  esumcvg  33370  signstres  33872  hgt750lemb  33954  revpfxsfxrev  34392  subfacp1lem4  34460  cvmliftmolem2  34559  msubff1  34833  iprodefisumlem  35002  poimirlem8  36799  poimirlem13  36804  poimirlem14  36805  ftc1cnnc  36863  eqlkr3  38274  cdleme51finvN  39730  sticksstones11  41278  metakunt33  41323  ofun  41364  frlmvscadiccat  41386  evlsvvval  41437  fsuppind  41464  ismrcd2  41739  ofoafo  42408  ofoaid1  42410  ofoaid2  42411  ofoaass  42412  ofoacom  42413  naddcnffo  42416  naddcnfcom  42418  naddcnfid1  42419  naddcnfass  42421  rfovcnvf1od  43057  dssmapntrcls  43181  dvconstbi  43395  fsumsermpt  44594  icccncfext  44902  voliooicof  45011  etransclem35  45284  rrxsnicc  45315  ovolval4lem1  45664  fcores  46076  zrinitorngc  46987  zrtermorngc  46988  zrtermoringc  47057  1arymaptf1  47416  2arymaptf1  47427