Theorem eqfnfvd 7028

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079   Fn wfn 6531  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-fv 6544

This theorem is referenced by:  foeqcnvco  7298  f1eqcocnv  7299  offveq  7700  tfrlem1  8358  updjudhcoinlf  9914  updjudhcoinrg  9915  ackbij2lem2  10218  ackbij2lem3  10219  fpwwe2lem7  10617  seqfeq2  14057  seqfeq  14059  seqfeq3  14084  ccatlid  14620  ccatrid  14621  ccatass  14622  ccatswrd  14702  swrdccat2  14703  pfxid  14718  ccatpfx  14734  pfxccat1  14735  swrdswrd  14738  cats1un  14754  swrdccatin1  14758  swrdccatin2  14762  pfxccatin12  14766  revccat  14799  revrev  14800  cshco  14869  swrdco  14870  seqshft  15118  seq1st  16624  xpsfeq  17612  yonedainv  18332  pwsco1mhm  18886  ghmquskerco  19349  f1otrspeq  19512  pmtrfinv  19526  symgtrinv  19537  frgpup3lem  19842  ablfac1eu  20140  zrinitorngc  20741  zrtermorngc  20742  zrtermoringc  20774  psgndiflemB  21750  frlmup1  21948  frlmup3  21950  frlmup4  21951  psrlidm  22111  psrridm  22112  psrass1  22113  subrgascl  22217  evlslem1  22233  evlsvvval  22244  psdmplcl  22325  psdvsca  22327  mavmulass  22706  upxp  23780  uptx  23782  cnextfres1  24225  ovolshftlem1  25668  volsup  25715  dvidlem  26074  dvrec  26114  dveq0  26159  dv11cn  26160  ftc1cn  26202  coemulc  26412  aannenlem1  26491  ulmuni  26555  ulmdv  26566  ostthlem1  27791  nvinvfval  30992  sspn  31088  kbass2  32469  xppreima2  32996  fdifsuppconst  33034  indpreima  33185  psgnfzto1stlem  33420  cycpmco2  33453  cyc3co2  33460  ply1gsumz  33889  mplasclco  33906  esplyind  33965  esumcvg  34476  signstres  34962  hgt750lemb  35043  revpfxsfxrev  35607  subfacp1lem4  35675  cvmliftmolem2  35774  msubff1  36048  iprodefisumlem  36232  poimirlem8  38279  poimirlem13  38284  poimirlem14  38285  ftc1cnnc  38343  eqlkr3  39875  cdleme51finvN  41330  sticksstones11  42923  aks6d1c6lem4  42940  ofun  43006  frlmvscadiccat  43280  fiabv  43304  fsuppind  43322  ismrcd2  43430  ofoafo  44083  ofoaid1  44085  ofoaid2  44086  ofoaass  44087  ofoacom  44088  naddcnffo  44091  naddcnfcom  44093  naddcnfid1  44094  naddcnfass  44096  rfovcnvf1od  44730  dssmapntrcls  44854  dvconstbi  45044  fsumsermpt  46295  icccncfext  46601  voliooicof  46710  etransclem35  46983  rrxsnicc  47014  ovolval4lem1  47363  fcores  47804  1arymaptf1  49422  2arymaptf1  49433  tposideq  49666  fucoid  50126  prcofdiag1  50171  prcofdiag  50172  oppfdiag1  50192  oppfdiag  50194  funcsn  50319