Theorem eqfnfvd 7054

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 3146	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
3		eqfnfvd.1	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4		eqfnfvd.2	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴)
5		eqfnfv 7051	. . 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 1540   ∈ wcel 2108  ∀wral 3061   Fn wfn 6556  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-fv 6569

This theorem is referenced by:  foeqcnvco  7320  f1eqcocnv  7321  offveq  7723  tfrlem1  8416  updjudhcoinlf  9972  updjudhcoinrg  9973  ackbij2lem2  10279  ackbij2lem3  10280  fpwwe2lem7  10677  seqfeq2  14066  seqfeq  14068  seqfeq3  14093  ccatlid  14624  ccatrid  14625  ccatass  14626  ccatswrd  14706  swrdccat2  14707  pfxid  14722  ccatpfx  14739  pfxccat1  14740  swrdswrd  14743  cats1un  14759  swrdccatin1  14763  swrdccatin2  14767  pfxccatin12  14771  revccat  14804  revrev  14805  cshco  14875  swrdco  14876  seqshft  15124  seq1st  16608  xpsfeq  17608  yonedainv  18326  pwsco1mhm  18845  ghmquskerco  19302  f1otrspeq  19465  pmtrfinv  19479  symgtrinv  19490  frgpup3lem  19795  ablfac1eu  20093  zrinitorngc  20642  zrtermorngc  20643  zrtermoringc  20675  psgndiflemB  21618  frlmup1  21818  frlmup3  21820  frlmup4  21821  psrlidm  21982  psrridm  21983  psrass1  21984  subrgascl  22090  evlslem1  22106  psdmplcl  22166  psdvsca  22168  mavmulass  22555  upxp  23631  uptx  23633  cnextfres1  24076  ovolshftlem1  25544  volsup  25591  dvidlem  25950  dvrec  25993  dveq0  26039  dv11cn  26040  ftc1cn  26084  coemulc  26294  aannenlem1  26370  ulmuni  26435  ulmdv  26446  ostthlem1  27671  nvinvfval  30659  sspn  30755  kbass2  32136  xppreima2  32661  fdifsuppconst  32698  indpreima  32850  psgnfzto1stlem  33120  cycpmco2  33153  cyc3co2  33160  ply1gsumz  33619  esumcvg  34087  signstres  34590  hgt750lemb  34671  revpfxsfxrev  35121  subfacp1lem4  35188  cvmliftmolem2  35287  msubff1  35561  iprodefisumlem  35740  poimirlem8  37635  poimirlem13  37640  poimirlem14  37641  ftc1cnnc  37699  eqlkr3  39102  cdleme51finvN  40558  sticksstones11  42157  aks6d1c6lem4  42174  metakunt33  42238  ofun  42277  frlmvscadiccat  42516  fiabv  42546  evlsvvval  42573  fsuppind  42600  ismrcd2  42710  ofoafo  43369  ofoaid1  43371  ofoaid2  43372  ofoaass  43373  ofoacom  43374  naddcnffo  43377  naddcnfcom  43379  naddcnfid1  43380  naddcnfass  43382  rfovcnvf1od  44017  dssmapntrcls  44141  dvconstbi  44353  fsumsermpt  45594  icccncfext  45902  voliooicof  46011  etransclem35  46284  rrxsnicc  46315  ovolval4lem1  46664  fcores  47079  1arymaptf1  48563  2arymaptf1  48574  tposideq  48788  fucoid  49043