Theorem eqfnfvd 7063

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∀wral 3080   Fn wfn 6561  ‘cfv 6566

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-fv 6574

This theorem is used by:  foeqcnvco  7339  f1eqcocnv  7340  offveq  7751  tfrlem1  8421  updjudhcoinlf  10050  updjudhcoinrg  10051  ackbij2lem2  10356  ackbij2lem3  10357  fpwwe2lem7  10761  seqfeq2  14208  seqfeq  14210  seqfeq3  14235  ccatlid  14773  ccatrid  14774  ccatass  14775  ccatswrd  14860  swrdccat2  14861  pfxid  14876  ccatpfx  14892  pfxccat1  14893  swrdswrd  14896  cats1un  14912  swrdccatin1  14916  swrdccatin2  14920  pfxccatin12  14924  revccat  14957  revrev  14958  revpfxsfxrev  14959  cshco  15029  swrdco  15030  seqshft  15281  seq1st  16790  xpsfeq  17785  yonedainv  18505  mgmn0plusgplusf  18878  pwsco1mhm  19078  ghmquskerco  19549  f1otrspeq  19712  pmtrfinv  19726  symgtrinv  19737  frgpup3lem  20042  ablfac1eu  20340  zrinitorngc  20945  zrtermorngc  20946  zrtermoringc  20978  psgndiflemB  21961  frlmup1  22159  frlmup3  22161  frlmup4  22162  psrlidm  22324  psrridm  22325  psrass1  22326  subrgascl  22430  evlslem1  22446  evlsvvval  22457  psdmplcl  22538  psdvsca  22540  mavmulass  22919  upxp  23997  uptx  23999  cnextfres1  24442  ovolshftlem1  25885  volsup  25932  dvidlem  26290  dvrec  26330  dveq0  26375  dv11cn  26376  ftc1cn  26418  coemulc  26629  aannenlem1  26712  ulmuni  26776  ulmdv  26787  ostthlem1  28011  nvinvfval  31299  sspn  31395  kbass2  32776  xppreima2  33343  fdifsuppconst  33379  indpreima  33528  psgnfzto1stlem  33760  cycpmco2  33793  cyc3co2  33800  ply1gsumz  34234  mplasclco  34259  esplyind  34318  esumcvg  34829  signstres  35315  hgt750lemb  35396  subfacp1lem4  36156  cvmliftmolem2  36255  msubff1  36529  iprodefisumlem  36720  poimirlem8  38814  poimirlem13  38819  poimirlem14  38820  ftc1cnnc  38878  eqlkr3  40424  cdleme51finvN  41879  sticksstones11  43472  aks6d1c6lem4  43489  ofun  43556  frlmvscadiccat  43839  fiabv  43866  fsuppind  43884  ismrcd2  43976  ofoafo  44619  ofoaid1  44621  ofoaid2  44622  ofoaass  44623  ofoacom  44624  naddcnffo  44627  naddcnfcom  44629  naddcnfid1  44630  naddcnfass  44632  rfovcnvf1od  45265  dssmapntrcls  45389  dvconstbi  45579  fsumsermpt  46864  icccncfext  47170  voliooicof  47279  etransclem35  47552  rrxsnicc  47583  ovolval4lem1  47932  fcores  48410  1arymaptf1  50085  2arymaptf1  50096  tposideq  50332  fucoid  50801  prcofdiag1  50859  prcofdiag  50860  oppfdiag1  50880  oppfdiag  50882  funcsn  51010  crosspaltd  51394  crossp3d  51395  veronesevrowd  51407