Theorem eqfnfvd 6988

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052   Fn wfn 6495  ‘cfv 6500

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-fv 6508

This theorem is referenced by:  foeqcnvco  7256  f1eqcocnv  7257  offveq  7658  tfrlem1  8317  updjudhcoinlf  9856  updjudhcoinrg  9857  ackbij2lem2  10161  ackbij2lem3  10162  fpwwe2lem7  10560  seqfeq2  13960  seqfeq  13962  seqfeq3  13987  ccatlid  14522  ccatrid  14523  ccatass  14524  ccatswrd  14604  swrdccat2  14605  pfxid  14620  ccatpfx  14636  pfxccat1  14637  swrdswrd  14640  cats1un  14656  swrdccatin1  14660  swrdccatin2  14664  pfxccatin12  14668  revccat  14701  revrev  14702  cshco  14771  swrdco  14772  seqshft  15020  seq1st  16510  xpsfeq  17496  yonedainv  18216  pwsco1mhm  18769  ghmquskerco  19225  f1otrspeq  19388  pmtrfinv  19402  symgtrinv  19413  frgpup3lem  19718  ablfac1eu  20016  zrinitorngc  20587  zrtermorngc  20588  zrtermoringc  20620  psgndiflemB  21567  frlmup1  21765  frlmup3  21767  frlmup4  21768  psrlidm  21929  psrridm  21930  psrass1  21931  subrgascl  22033  evlslem1  22049  evlsvvval  22060  psdmplcl  22117  psdvsca  22119  mavmulass  22505  upxp  23579  uptx  23581  cnextfres1  24024  ovolshftlem1  25478  volsup  25525  dvidlem  25884  dvrec  25927  dveq0  25973  dv11cn  25974  ftc1cn  26018  coemulc  26228  aannenlem1  26304  ulmuni  26369  ulmdv  26380  ostthlem1  27606  nvinvfval  30728  sspn  30824  kbass2  32205  xppreima2  32741  fdifsuppconst  32779  indpreima  32958  psgnfzto1stlem  33194  cycpmco2  33227  cyc3co2  33234  ply1gsumz  33692  esplyind  33752  esumcvg  34264  signstres  34753  hgt750lemb  34834  revpfxsfxrev  35332  subfacp1lem4  35399  cvmliftmolem2  35498  msubff1  35772  iprodefisumlem  35956  poimirlem8  37879  poimirlem13  37884  poimirlem14  37885  ftc1cnnc  37943  eqlkr3  39477  cdleme51finvN  40932  sticksstones11  42526  aks6d1c6lem4  42543  ofun  42608  frlmvscadiccat  42876  fiabv  42906  fsuppind  42948  ismrcd2  43056  ofoafo  43713  ofoaid1  43715  ofoaid2  43716  ofoaass  43717  ofoacom  43718  naddcnffo  43721  naddcnfcom  43723  naddcnfid1  43724  naddcnfass  43726  rfovcnvf1od  44360  dssmapntrcls  44484  dvconstbi  44690  fsumsermpt  45939  icccncfext  46245  voliooicof  46354  etransclem35  46627  rrxsnicc  46658  ovolval4lem1  47007  fcores  47427  1arymaptf1  49002  2arymaptf1  49013  tposideq  49247  fucoid  49707  prcofdiag1  49752  prcofdiag  49753  oppfdiag1  49773  oppfdiag  49775  funcsn  49900