Theorem eqfnfvd 7032

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 3159	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
3		eqfnfvd.1	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4		eqfnfvd.2	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴)
5		eqfnfv 7029	. . 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 2146  ∀wral 3081   Fn wfn 6535  ‘cfv 6540

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

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 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-fv 6548

This theorem is used by:  foeqcnvco  7307  f1eqcocnv  7308  offveq  7710  tfrlem1  8368  updjudhcoinlf  9934  updjudhcoinrg  9935  ackbij2lem2  10238  ackbij2lem3  10239  fpwwe2lem7  10637  seqfeq2  14079  seqfeq  14081  seqfeq3  14106  ccatlid  14642  ccatrid  14643  ccatass  14644  ccatswrd  14728  swrdccat2  14729  pfxid  14744  ccatpfx  14760  pfxccat1  14761  swrdswrd  14764  cats1un  14780  swrdccatin1  14784  swrdccatin2  14788  pfxccatin12  14792  revccat  14825  revrev  14826  revpfxsfxrev  14827  cshco  14897  swrdco  14898  seqshft  15146  seq1st  16651  xpsfeq  17639  yonedainv  18359  mgmn0plusgplusf  18732  pwsco1mhm  18928  ghmquskerco  19398  f1otrspeq  19561  pmtrfinv  19575  symgtrinv  19586  frgpup3lem  19891  ablfac1eu  20189  zrinitorngc  20791  zrtermorngc  20792  zrtermoringc  20824  psgndiflemB  21800  frlmup1  21998  frlmup3  22000  frlmup4  22001  psrlidm  22161  psrridm  22162  psrass1  22163  subrgascl  22267  evlslem1  22283  evlsvvval  22294  psdmplcl  22375  psdvsca  22377  mavmulass  22756  upxp  23831  uptx  23833  cnextfres1  24276  ovolshftlem1  25719  volsup  25766  dvidlem  26125  dvrec  26165  dveq0  26210  dv11cn  26211  ftc1cn  26253  coemulc  26463  aannenlem1  26542  ulmuni  26606  ulmdv  26617  ostthlem1  27842  nvinvfval  31063  sspn  31159  kbass2  32540  xppreima2  33067  fdifsuppconst  33105  indpreima  33255  psgnfzto1stlem  33484  cycpmco2  33517  cyc3co2  33524  ply1gsumz  33953  mplasclco  33970  esplyind  34029  esumcvg  34540  signstres  35027  hgt750lemb  35108  subfacp1lem4  35712  cvmliftmolem2  35811  msubff1  36085  iprodefisumlem  36269  poimirlem8  38336  poimirlem13  38341  poimirlem14  38342  ftc1cnnc  38400  eqlkr3  39933  cdleme51finvN  41388  sticksstones11  42981  aks6d1c6lem4  42998  ofun  43064  frlmvscadiccat  43338  fiabv  43362  fsuppind  43380  ismrcd2  43488  ofoafo  44141  ofoaid1  44143  ofoaid2  44144  ofoaass  44145  ofoacom  44146  naddcnffo  44149  naddcnfcom  44151  naddcnfid1  44152  naddcnfass  44154  rfovcnvf1od  44788  dssmapntrcls  44912  dvconstbi  45102  fsumsermpt  46353  icccncfext  46659  voliooicof  46768  etransclem35  47041  rrxsnicc  47072  ovolval4lem1  47421  fcores  47862  1arymaptf1  49479  2arymaptf1  49490  tposideq  49723  fucoid  50183  prcofdiag1  50228  prcofdiag  50229  oppfdiag1  50249  oppfdiag  50251  funcsn  50376  crosspaltd  50705  crossp3d  50706