Theorem eqfnfvd 6976

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 3125	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
3		eqfnfvd.1	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4		eqfnfvd.2	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴)
5		eqfnfv 6973	. . 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 1541   ∈ wcel 2113  ∀wral 3048   Fn wfn 6484  ‘cfv 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-fv 6497

This theorem is referenced by:  foeqcnvco  7243  f1eqcocnv  7244  offveq  7645  tfrlem1  8304  updjudhcoinlf  9836  updjudhcoinrg  9837  ackbij2lem2  10141  ackbij2lem3  10142  fpwwe2lem7  10539  seqfeq2  13939  seqfeq  13941  seqfeq3  13966  ccatlid  14501  ccatrid  14502  ccatass  14503  ccatswrd  14583  swrdccat2  14584  pfxid  14599  ccatpfx  14615  pfxccat1  14616  swrdswrd  14619  cats1un  14635  swrdccatin1  14639  swrdccatin2  14643  pfxccatin12  14647  revccat  14680  revrev  14681  cshco  14750  swrdco  14751  seqshft  14999  seq1st  16489  xpsfeq  17475  yonedainv  18195  pwsco1mhm  18748  ghmquskerco  19204  f1otrspeq  19367  pmtrfinv  19381  symgtrinv  19392  frgpup3lem  19697  ablfac1eu  19995  zrinitorngc  20566  zrtermorngc  20567  zrtermoringc  20599  psgndiflemB  21546  frlmup1  21744  frlmup3  21746  frlmup4  21747  psrlidm  21908  psrridm  21909  psrass1  21910  subrgascl  22012  evlslem1  22028  evlsvvval  22039  psdmplcl  22096  psdvsca  22098  mavmulass  22484  upxp  23558  uptx  23560  cnextfres1  24003  ovolshftlem1  25457  volsup  25504  dvidlem  25863  dvrec  25906  dveq0  25952  dv11cn  25953  ftc1cn  25997  coemulc  26207  aannenlem1  26283  ulmuni  26348  ulmdv  26359  ostthlem1  27585  nvinvfval  30641  sspn  30737  kbass2  32118  xppreima2  32655  fdifsuppconst  32694  indpreima  32875  psgnfzto1stlem  33110  cycpmco2  33143  cyc3co2  33150  ply1gsumz  33608  esplyind  33659  esumcvg  34171  signstres  34660  hgt750lemb  34741  revpfxsfxrev  35232  subfacp1lem4  35299  cvmliftmolem2  35398  msubff1  35672  iprodefisumlem  35856  poimirlem8  37741  poimirlem13  37746  poimirlem14  37747  ftc1cnnc  37805  eqlkr3  39273  cdleme51finvN  40728  sticksstones11  42322  aks6d1c6lem4  42339  ofun  42407  frlmvscadiccat  42676  fiabv  42706  fsuppind  42748  ismrcd2  42856  ofoafo  43513  ofoaid1  43515  ofoaid2  43516  ofoaass  43517  ofoacom  43518  naddcnffo  43521  naddcnfcom  43523  naddcnfid1  43524  naddcnfass  43526  rfovcnvf1od  44161  dssmapntrcls  44285  dvconstbi  44491  fsumsermpt  45741  icccncfext  46047  voliooicof  46156  etransclem35  46429  rrxsnicc  46460  ovolval4lem1  46809  fcores  47229  1arymaptf1  48804  2arymaptf1  48815  tposideq  49049  fucoid  49509  prcofdiag1  49554  prcofdiag  49555  oppfdiag1  49575  oppfdiag  49577  funcsn  49702