Theorem eqfnfvd 7053

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 3143	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
3		eqfnfvd.1	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4		eqfnfvd.2	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴)
5		eqfnfv 7050	. . 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 1536   ∈ wcel 2105  ∀wral 3058   Fn wfn 6557  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-fv 6570

This theorem is referenced by:  foeqcnvco  7319  f1eqcocnv  7320  offveq  7722  tfrlem1  8414  updjudhcoinlf  9969  updjudhcoinrg  9970  ackbij2lem2  10276  ackbij2lem3  10277  fpwwe2lem7  10674  seqfeq2  14062  seqfeq  14064  seqfeq3  14089  ccatlid  14620  ccatrid  14621  ccatass  14622  ccatswrd  14702  swrdccat2  14703  pfxid  14718  ccatpfx  14735  pfxccat1  14736  swrdswrd  14739  cats1un  14755  swrdccatin1  14759  swrdccatin2  14763  pfxccatin12  14767  revccat  14800  revrev  14801  cshco  14871  swrdco  14872  seqshft  15120  seq1st  16604  xpsfeq  17609  yonedainv  18337  pwsco1mhm  18857  ghmquskerco  19314  f1otrspeq  19479  pmtrfinv  19493  symgtrinv  19504  frgpup3lem  19809  ablfac1eu  20107  zrinitorngc  20658  zrtermorngc  20659  zrtermoringc  20691  psgndiflemB  21635  frlmup1  21835  frlmup3  21837  frlmup4  21838  psrlidm  21999  psrridm  22000  psrass1  22001  subrgascl  22107  evlslem1  22123  psdmplcl  22183  psdvsca  22185  mavmulass  22570  upxp  23646  uptx  23648  cnextfres1  24091  ovolshftlem1  25557  volsup  25604  dvidlem  25964  dvrec  26007  dveq0  26053  dv11cn  26054  ftc1cn  26098  coemulc  26308  aannenlem1  26384  ulmuni  26449  ulmdv  26460  ostthlem1  27685  nvinvfval  30668  sspn  30764  kbass2  32145  xppreima2  32667  fdifsuppconst  32703  psgnfzto1stlem  33102  cycpmco2  33135  cyc3co2  33142  ply1gsumz  33598  indpreima  34005  esumcvg  34066  signstres  34568  hgt750lemb  34649  revpfxsfxrev  35099  subfacp1lem4  35167  cvmliftmolem2  35266  msubff1  35540  iprodefisumlem  35719  poimirlem8  37614  poimirlem13  37619  poimirlem14  37620  ftc1cnnc  37678  eqlkr3  39082  cdleme51finvN  40538  sticksstones11  42137  aks6d1c6lem4  42154  metakunt33  42218  ofun  42255  frlmvscadiccat  42492  fiabv  42522  evlsvvval  42549  fsuppind  42576  ismrcd2  42686  ofoafo  43345  ofoaid1  43347  ofoaid2  43348  ofoaass  43349  ofoacom  43350  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  naddcnfass  43358  rfovcnvf1od  43993  dssmapntrcls  44117  dvconstbi  44329  fsumsermpt  45534  icccncfext  45842  voliooicof  45951  etransclem35  46224  rrxsnicc  46255  ovolval4lem1  46604  fcores  47016  1arymaptf1  48491  2arymaptf1  48502