Theorem eqfnfvd 7037

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076   Fn wfn 6538  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6497  df-fun 6545  df-fn 6546  df-fv 6551

This theorem is used by:  foeqcnvco  7312  f1eqcocnv  7313  offveq  7723  tfrlem1  8390  updjudhcoinlf  10020  updjudhcoinrg  10021  ackbij2lem2  10324  ackbij2lem3  10325  fpwwe2lem7  10729  seqfeq2  14175  seqfeq  14177  seqfeq3  14202  ccatlid  14739  ccatrid  14740  ccatass  14741  ccatswrd  14826  swrdccat2  14827  pfxid  14842  ccatpfx  14858  pfxccat1  14859  swrdswrd  14862  cats1un  14878  swrdccatin1  14882  swrdccatin2  14886  pfxccatin12  14890  revccat  14923  revrev  14924  revpfxsfxrev  14925  cshco  14995  swrdco  14996  seqshft  15247  seq1st  16755  xpsfeq  17744  yonedainv  18464  mgmn0plusgplusf  18837  pwsco1mhm  19037  ghmquskerco  19507  f1otrspeq  19670  pmtrfinv  19684  symgtrinv  19695  frgpup3lem  20000  ablfac1eu  20298  zrinitorngc  20903  zrtermorngc  20904  zrtermoringc  20936  psgndiflemB  21915  frlmup1  22113  frlmup3  22115  frlmup4  22116  psrlidm  22278  psrridm  22279  psrass1  22280  subrgascl  22384  evlslem1  22400  evlsvvval  22411  psdmplcl  22492  psdvsca  22494  mavmulass  22873  upxp  23951  uptx  23953  cnextfres1  24396  ovolshftlem1  25839  volsup  25886  dvidlem  26244  dvrec  26284  dveq0  26329  dv11cn  26330  ftc1cn  26372  coemulc  26583  aannenlem1  26664  ulmuni  26728  ulmdv  26739  ostthlem1  27963  nvinvfval  31251  sspn  31347  kbass2  32728  xppreima2  33296  fdifsuppconst  33333  indpreima  33482  psgnfzto1stlem  33711  cycpmco2  33744  cyc3co2  33751  ply1gsumz  34181  mplasclco  34198  esplyind  34257  esumcvg  34768  signstres  35254  hgt750lemb  35335  subfacp1lem4  36038  cvmliftmolem2  36137  msubff1  36411  iprodefisumlem  36601  poimirlem8  38655  poimirlem13  38660  poimirlem14  38661  ftc1cnnc  38719  eqlkr3  40267  cdleme51finvN  41722  sticksstones11  43315  aks6d1c6lem4  43332  ofun  43398  frlmvscadiccat  43682  fiabv  43709  fsuppind  43727  ismrcd2  43819  ofoafo  44467  ofoaid1  44469  ofoaid2  44470  ofoaass  44471  ofoacom  44472  naddcnffo  44475  naddcnfcom  44477  naddcnfid1  44478  naddcnfass  44480  rfovcnvf1od  45113  dssmapntrcls  45237  dvconstbi  45427  fsumsermpt  46699  icccncfext  47005  voliooicof  47114  etransclem35  47387  rrxsnicc  47418  ovolval4lem1  47767  fcores  48245  1arymaptf1  49862  2arymaptf1  49873  tposideq  50109  fucoid  50578  prcofdiag1  50636  prcofdiag  50637  oppfdiag1  50657  oppfdiag  50659  funcsn  50787  crosspaltd  51149  crossp3d  51150  veronesevrowd  51162