Theorem eqfnfvd 6990

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3060   Fn wfn 6496  ‘cfv 6501

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-fv 6509

This theorem is referenced by:  foeqcnvco  7251  f1eqcocnv  7252  f1eqcocnvOLD  7253  offveq  7646  tfrlem1  8327  updjudhcoinlf  9877  updjudhcoinrg  9878  ackbij2lem2  10185  ackbij2lem3  10186  fpwwe2lem7  10582  seqfeq2  13941  seqfeq  13943  seqfeq3  13968  ccatlid  14486  ccatrid  14487  ccatass  14488  ccatswrd  14568  swrdccat2  14569  pfxid  14584  ccatpfx  14601  pfxccat1  14602  swrdswrd  14605  cats1un  14621  swrdccatin1  14625  swrdccatin2  14629  pfxccatin12  14633  revccat  14666  revrev  14667  cshco  14737  swrdco  14738  seqshft  14982  seq1st  16458  xpsfeq  17459  yonedainv  18184  pwsco1mhm  18656  f1otrspeq  19243  pmtrfinv  19257  symgtrinv  19268  frgpup3lem  19573  ablfac1eu  19866  psgndiflemB  21041  frlmup1  21241  frlmup3  21243  frlmup4  21244  psrlidm  21409  psrridm  21410  psrass1  21411  subrgascl  21511  evlslem1  21529  mavmulass  21935  upxp  23011  uptx  23013  cnextfres1  23456  ovolshftlem1  24910  volsup  24957  dvidlem  25316  dvrec  25356  dveq0  25401  dv11cn  25402  ftc1cn  25444  coemulc  25653  aannenlem1  25725  ulmuni  25788  ulmdv  25799  ostthlem1  27012  nvinvfval  29645  sspn  29741  kbass2  31122  xppreima2  31634  fdifsuppconst  31671  psgnfzto1stlem  32019  cycpmco2  32052  cyc3co2  32059  ghmquskerco  32270  ply1gsumz  32368  indpreima  32713  esumcvg  32774  signstres  33276  hgt750lemb  33358  revpfxsfxrev  33796  subfacp1lem4  33864  cvmliftmolem2  33963  msubff1  34237  iprodefisumlem  34399  poimirlem8  36159  poimirlem13  36164  poimirlem14  36165  ftc1cnnc  36223  eqlkr3  37636  cdleme51finvN  39092  sticksstones11  40637  metakunt33  40682  ofun  40731  frlmvscadiccat  40749  evlsbagval  40806  fsuppind  40823  ismrcd2  41080  ofoafo  41749  ofoaid1  41751  ofoaid2  41752  ofoaass  41753  ofoacom  41754  naddcnffo  41757  naddcnfcom  41759  naddcnfid1  41760  naddcnfass  41762  rfovcnvf1od  42398  dssmapntrcls  42522  dvconstbi  42736  fsumsermpt  43940  icccncfext  44248  voliooicof  44357  etransclem35  44630  rrxsnicc  44661  ovolval4lem1  45010  fcores  45421  zrinitorngc  46418  zrtermorngc  46419  zrtermoringc  46488  1arymaptf1  46848  2arymaptf1  46859