Theorem eqfnfvd 7006

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 7003	. . 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 2109  ∀wral 3044   Fn wfn 6506  ‘cfv 6511

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  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 6464  df-fun 6513  df-fn 6514  df-fv 6519

This theorem is referenced by:  foeqcnvco  7275  f1eqcocnv  7276  offveq  7679  tfrlem1  8344  updjudhcoinlf  9885  updjudhcoinrg  9886  ackbij2lem2  10192  ackbij2lem3  10193  fpwwe2lem7  10590  seqfeq2  13990  seqfeq  13992  seqfeq3  14017  ccatlid  14551  ccatrid  14552  ccatass  14553  ccatswrd  14633  swrdccat2  14634  pfxid  14649  ccatpfx  14666  pfxccat1  14667  swrdswrd  14670  cats1un  14686  swrdccatin1  14690  swrdccatin2  14694  pfxccatin12  14698  revccat  14731  revrev  14732  cshco  14802  swrdco  14803  seqshft  15051  seq1st  16541  xpsfeq  17526  yonedainv  18242  pwsco1mhm  18759  ghmquskerco  19216  f1otrspeq  19377  pmtrfinv  19391  symgtrinv  19402  frgpup3lem  19707  ablfac1eu  20005  zrinitorngc  20551  zrtermorngc  20552  zrtermoringc  20584  psgndiflemB  21509  frlmup1  21707  frlmup3  21709  frlmup4  21710  psrlidm  21871  psrridm  21872  psrass1  21873  subrgascl  21973  evlslem1  21989  psdmplcl  22049  psdvsca  22051  mavmulass  22436  upxp  23510  uptx  23512  cnextfres1  23955  ovolshftlem1  25410  volsup  25457  dvidlem  25816  dvrec  25859  dveq0  25905  dv11cn  25906  ftc1cn  25950  coemulc  26160  aannenlem1  26236  ulmuni  26301  ulmdv  26312  ostthlem1  27538  nvinvfval  30569  sspn  30665  kbass2  32046  xppreima2  32575  fdifsuppconst  32612  indpreima  32788  psgnfzto1stlem  33057  cycpmco2  33090  cyc3co2  33097  ply1gsumz  33564  esumcvg  34076  signstres  34566  hgt750lemb  34647  revpfxsfxrev  35103  subfacp1lem4  35170  cvmliftmolem2  35269  msubff1  35543  iprodefisumlem  35727  poimirlem8  37622  poimirlem13  37627  poimirlem14  37628  ftc1cnnc  37686  eqlkr3  39094  cdleme51finvN  40550  sticksstones11  42144  aks6d1c6lem4  42161  ofun  42224  frlmvscadiccat  42494  fiabv  42524  evlsvvval  42551  fsuppind  42578  ismrcd2  42687  ofoafo  43345  ofoaid1  43347  ofoaid2  43348  ofoaass  43349  ofoacom  43350  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  naddcnfass  43358  rfovcnvf1od  43993  dssmapntrcls  44117  dvconstbi  44323  fsumsermpt  45577  icccncfext  45885  voliooicof  45994  etransclem35  46267  rrxsnicc  46298  ovolval4lem1  46647  fcores  47068  1arymaptf1  48631  2arymaptf1  48642  tposideq  48876  fucoid  49337  prcofdiag1  49382  prcofdiag  49383  oppfdiag1  49403  oppfdiag  49405  funcsn  49530