Theorem eqfnfvd 6986

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 3129	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
3		eqfnfvd.1	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4		eqfnfvd.2	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴)
5		eqfnfv 6983	. . 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 3051   Fn wfn 6493  ‘cfv 6498

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-fv 6506

This theorem is referenced by:  foeqcnvco  7255  f1eqcocnv  7256  offveq  7657  tfrlem1  8315  updjudhcoinlf  9856  updjudhcoinrg  9857  ackbij2lem2  10161  ackbij2lem3  10162  fpwwe2lem7  10560  seqfeq2  13987  seqfeq  13989  seqfeq3  14014  ccatlid  14549  ccatrid  14550  ccatass  14551  ccatswrd  14631  swrdccat2  14632  pfxid  14647  ccatpfx  14663  pfxccat1  14664  swrdswrd  14667  cats1un  14683  swrdccatin1  14687  swrdccatin2  14691  pfxccatin12  14695  revccat  14728  revrev  14729  cshco  14798  swrdco  14799  seqshft  15047  seq1st  16540  xpsfeq  17527  yonedainv  18247  pwsco1mhm  18800  ghmquskerco  19259  f1otrspeq  19422  pmtrfinv  19436  symgtrinv  19447  frgpup3lem  19752  ablfac1eu  20050  zrinitorngc  20619  zrtermorngc  20620  zrtermoringc  20652  psgndiflemB  21580  frlmup1  21778  frlmup3  21780  frlmup4  21781  psrlidm  21940  psrridm  21941  psrass1  21942  subrgascl  22044  evlslem1  22060  evlsvvval  22071  psdmplcl  22128  psdvsca  22130  mavmulass  22514  upxp  23588  uptx  23590  cnextfres1  24033  ovolshftlem1  25476  volsup  25523  dvidlem  25882  dvrec  25922  dveq0  25967  dv11cn  25968  ftc1cn  26010  coemulc  26220  aannenlem1  26294  ulmuni  26357  ulmdv  26368  ostthlem1  27590  nvinvfval  30711  sspn  30807  kbass2  32188  xppreima2  32724  fdifsuppconst  32762  indpreima  32925  psgnfzto1stlem  33161  cycpmco2  33194  cyc3co2  33201  ply1gsumz  33659  esplyind  33719  esumcvg  34230  signstres  34719  hgt750lemb  34800  revpfxsfxrev  35298  subfacp1lem4  35365  cvmliftmolem2  35464  msubff1  35738  iprodefisumlem  35922  poimirlem8  37949  poimirlem13  37954  poimirlem14  37955  ftc1cnnc  38013  eqlkr3  39547  cdleme51finvN  41002  sticksstones11  42595  aks6d1c6lem4  42612  ofun  42677  frlmvscadiccat  42951  fiabv  42981  fsuppind  43023  ismrcd2  43131  ofoafo  43784  ofoaid1  43786  ofoaid2  43787  ofoaass  43788  ofoacom  43789  naddcnffo  43792  naddcnfcom  43794  naddcnfid1  43795  naddcnfass  43797  rfovcnvf1od  44431  dssmapntrcls  44555  dvconstbi  44761  fsumsermpt  46009  icccncfext  46315  voliooicof  46424  etransclem35  46697  rrxsnicc  46728  ovolval4lem1  47077  fcores  47515  1arymaptf1  49118  2arymaptf1  49129  tposideq  49363  fucoid  49823  prcofdiag1  49868  prcofdiag  49869  oppfdiag1  49889  oppfdiag  49891  funcsn  50016