Theorem eqfnfvd 6906

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1541   ∈ wcel 2109  ∀wral 3065   Fn wfn 6425  ‘cfv 6430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-fv 6438

This theorem is referenced by:  foeqcnvco  7165  f1eqcocnv  7166  f1eqcocnvOLD  7167  offveq  7548  tfrlem1  8191  updjudhcoinlf  9674  updjudhcoinrg  9675  ackbij2lem2  9980  ackbij2lem3  9981  fpwwe2lem7  10377  seqfeq2  13727  seqfeq  13729  seqfeq3  13754  ccatlid  14272  ccatrid  14273  ccatass  14274  ccatswrd  14362  swrdccat2  14363  pfxid  14378  ccatpfx  14395  pfxccat1  14396  swrdswrd  14399  cats1un  14415  swrdccatin1  14419  swrdccatin2  14423  pfxccatin12  14427  revccat  14460  revrev  14461  cshco  14530  swrdco  14531  seqshft  14777  seq1st  16257  xpsfeq  17255  yonedainv  17980  pwsco1mhm  18451  f1otrspeq  19036  pmtrfinv  19050  symgtrinv  19061  frgpup3lem  19364  ablfac1eu  19657  psgndiflemB  20786  frlmup1  20986  frlmup3  20988  frlmup4  20989  psrlidm  21153  psrridm  21154  psrass1  21155  subrgascl  21255  evlslem1  21273  mavmulass  21679  upxp  22755  uptx  22757  cnextfres1  23200  ovolshftlem1  24654  volsup  24701  dvidlem  25060  dvrec  25100  dveq0  25145  dv11cn  25146  ftc1cn  25188  coemulc  25397  aannenlem1  25469  ulmuni  25532  ulmdv  25543  ostthlem1  26756  nvinvfval  28981  sspn  29077  kbass2  30458  xppreima2  30967  fdifsuppconst  31002  psgnfzto1stlem  31346  cycpmco2  31379  cyc3co2  31386  indpreima  31972  esumcvg  32033  signstres  32533  hgt750lemb  32615  revpfxsfxrev  33056  subfacp1lem4  33124  cvmliftmolem2  33223  msubff1  33497  iprodefisumlem  33685  poimirlem8  35764  poimirlem13  35769  poimirlem14  35770  ftc1cnnc  35828  eqlkr3  37094  cdleme51finvN  38549  sticksstones11  40092  metakunt33  40137  ofun  40191  frlmvscadiccat  40217  evlsbagval  40255  fsuppind  40259  ismrcd2  40501  rfovcnvf1od  41565  dssmapntrcls  41691  dvconstbi  41905  fsumsermpt  43074  icccncfext  43382  voliooicof  43491  etransclem35  43764  rrxsnicc  43795  ovolval4lem1  44141  fcores  44512  zrinitorngc  45510  zrtermorngc  45511  zrtermoringc  45580  1arymaptf1  45940  2arymaptf1  45951