Theorem eqfnfvd 6800

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∀wral 3138   Fn wfn 6345  ‘cfv 6350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-fv 6358

This theorem is referenced by:  foeqcnvco  7050  f1eqcocnv  7051  offveq  7424  tfrlem1  8006  updjudhcoinlf  9355  updjudhcoinrg  9356  ackbij2lem2  9656  ackbij2lem3  9657  fpwwe2lem8  10053  seqfeq2  13387  seqfeq  13389  seqfeq3  13414  ccatlid  13934  ccatrid  13935  ccatass  13936  ccatswrd  14024  swrdccat2  14025  pfxid  14040  ccatpfx  14057  pfxccat1  14058  swrdswrd  14061  cats1un  14077  swrdccatin1  14081  swrdccatin2  14085  pfxccatin12  14089  revccat  14122  revrev  14123  cshco  14192  swrdco  14193  seqshft  14438  seq1st  15909  xpsfeq  16830  yonedainv  17525  pwsco1mhm  17990  f1otrspeq  18569  pmtrfinv  18583  symgtrinv  18594  frgpup3lem  18897  ablfac1eu  19189  psrlidm  20177  psrridm  20178  psrass1  20179  subrgascl  20272  evlslem1  20289  psgndiflemB  20738  frlmup1  20936  frlmup3  20938  frlmup4  20939  mavmulass  21152  upxp  22225  uptx  22227  cnextfres1  22670  ovolshftlem1  24104  volsup  24151  dvidlem  24507  dvrec  24546  dveq0  24591  dv11cn  24592  ftc1cn  24634  coemulc  24839  aannenlem1  24911  ulmuni  24974  ulmdv  24985  ostthlem1  26197  nvinvfval  28411  sspn  28507  kbass2  29888  xppreima2  30389  psgnfzto1stlem  30737  cycpmco2  30770  cyc3co2  30777  indpreima  31279  esumcvg  31340  signstres  31840  hgt750lemb  31922  revpfxsfxrev  32357  subfacp1lem4  32425  cvmliftmolem2  32524  msubff1  32798  iprodefisumlem  32967  poimirlem8  34894  poimirlem13  34899  poimirlem14  34900  ftc1cnnc  34960  eqlkr3  36231  cdleme51finvN  37686  frlmvscadiccat  39138  ismrcd2  39289  rfovcnvf1od  40343  dssmapntrcls  40471  dvconstbi  40659  fsumsermpt  41852  icccncfext  42162  voliooicof  42274  etransclem35  42547  rrxsnicc  42578  ovolval4lem1  42924  zrinitorngc  44264  zrtermorngc  44265  zrtermoringc  44334