Theorem eqfnfvd 7067

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067   Fn wfn 6568  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-fv 6581

This theorem is referenced by:  foeqcnvco  7336  f1eqcocnv  7337  offveq  7739  tfrlem1  8432  updjudhcoinlf  10001  updjudhcoinrg  10002  ackbij2lem2  10308  ackbij2lem3  10309  fpwwe2lem7  10706  seqfeq2  14076  seqfeq  14078  seqfeq3  14103  ccatlid  14634  ccatrid  14635  ccatass  14636  ccatswrd  14716  swrdccat2  14717  pfxid  14732  ccatpfx  14749  pfxccat1  14750  swrdswrd  14753  cats1un  14769  swrdccatin1  14773  swrdccatin2  14777  pfxccatin12  14781  revccat  14814  revrev  14815  cshco  14885  swrdco  14886  seqshft  15134  seq1st  16618  xpsfeq  17623  yonedainv  18351  pwsco1mhm  18867  ghmquskerco  19324  f1otrspeq  19489  pmtrfinv  19503  symgtrinv  19514  frgpup3lem  19819  ablfac1eu  20117  zrinitorngc  20664  zrtermorngc  20665  zrtermoringc  20697  psgndiflemB  21641  frlmup1  21841  frlmup3  21843  frlmup4  21844  psrlidm  22005  psrridm  22006  psrass1  22007  subrgascl  22113  evlslem1  22129  psdmplcl  22189  psdvsca  22191  mavmulass  22576  upxp  23652  uptx  23654  cnextfres1  24097  ovolshftlem1  25563  volsup  25610  dvidlem  25970  dvrec  26013  dveq0  26059  dv11cn  26060  ftc1cn  26104  coemulc  26314  aannenlem1  26388  ulmuni  26453  ulmdv  26464  ostthlem1  27689  nvinvfval  30672  sspn  30768  kbass2  32149  xppreima2  32669  fdifsuppconst  32701  psgnfzto1stlem  33093  cycpmco2  33126  cyc3co2  33133  ply1gsumz  33584  indpreima  33989  esumcvg  34050  signstres  34552  hgt750lemb  34633  revpfxsfxrev  35083  subfacp1lem4  35151  cvmliftmolem2  35250  msubff1  35524  iprodefisumlem  35702  poimirlem8  37588  poimirlem13  37593  poimirlem14  37594  ftc1cnnc  37652  eqlkr3  39057  cdleme51finvN  40513  sticksstones11  42113  aks6d1c6lem4  42130  metakunt33  42194  ofun  42231  frlmvscadiccat  42461  fiabv  42491  evlsvvval  42518  fsuppind  42545  ismrcd2  42655  ofoafo  43318  ofoaid1  43320  ofoaid2  43321  ofoaass  43322  ofoacom  43323  naddcnffo  43326  naddcnfcom  43328  naddcnfid1  43329  naddcnfass  43331  rfovcnvf1od  43966  dssmapntrcls  44090  dvconstbi  44303  fsumsermpt  45500  icccncfext  45808  voliooicof  45917  etransclem35  46190  rrxsnicc  46221  ovolval4lem1  46570  fcores  46982  1arymaptf1  48376  2arymaptf1  48387