Theorem eqfnfvd 7030

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 3155	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
3		eqfnfvd.1	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4		eqfnfvd.2	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴)
5		eqfnfv 7027	. . 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 1570   ∈ wcel 2145  ∀wral 3077   Fn wfn 6532  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  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 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is used by:  foeqcnvco  7306  f1eqcocnv  7307  offveq  7717  tfrlem1  8376  updjudhcoinlf  10006  updjudhcoinrg  10007  ackbij2lem2  10310  ackbij2lem3  10311  fpwwe2lem7  10715  seqfeq2  14161  seqfeq  14163  seqfeq3  14188  ccatlid  14725  ccatrid  14726  ccatass  14727  ccatswrd  14811  swrdccat2  14812  pfxid  14827  ccatpfx  14843  pfxccat1  14844  swrdswrd  14847  cats1un  14863  swrdccatin1  14867  swrdccatin2  14871  pfxccatin12  14875  revccat  14908  revrev  14909  revpfxsfxrev  14910  cshco  14980  swrdco  14981  seqshft  15231  seq1st  16739  xpsfeq  17728  yonedainv  18448  mgmn0plusgplusf  18821  pwsco1mhm  19021  ghmquskerco  19491  f1otrspeq  19654  pmtrfinv  19668  symgtrinv  19679  frgpup3lem  19984  ablfac1eu  20282  zrinitorngc  20887  zrtermorngc  20888  zrtermoringc  20920  psgndiflemB  21899  frlmup1  22097  frlmup3  22099  frlmup4  22100  psrlidm  22262  psrridm  22263  psrass1  22264  subrgascl  22368  evlslem1  22384  evlsvvval  22395  psdmplcl  22476  psdvsca  22478  mavmulass  22857  upxp  23935  uptx  23937  cnextfres1  24380  ovolshftlem1  25823  volsup  25870  dvidlem  26228  dvrec  26268  dveq0  26313  dv11cn  26314  ftc1cn  26356  coemulc  26567  aannenlem1  26648  ulmuni  26712  ulmdv  26723  ostthlem1  27947  nvinvfval  31235  sspn  31331  kbass2  32712  xppreima2  33238  fdifsuppconst  33275  indpreima  33425  psgnfzto1stlem  33654  cycpmco2  33687  cyc3co2  33694  ply1gsumz  34124  mplasclco  34141  esplyind  34200  esumcvg  34711  signstres  35197  hgt750lemb  35278  subfacp1lem4  35927  cvmliftmolem2  36026  msubff1  36300  iprodefisumlem  36484  poimirlem8  38526  poimirlem13  38531  poimirlem14  38532  ftc1cnnc  38590  eqlkr3  40138  cdleme51finvN  41593  sticksstones11  43186  aks6d1c6lem4  43203  ofun  43269  frlmvscadiccat  43553  fiabv  43580  fsuppind  43598  ismrcd2  43689  ofoafo  44342  ofoaid1  44344  ofoaid2  44345  ofoaass  44346  ofoacom  44347  naddcnffo  44350  naddcnfcom  44352  naddcnfid1  44353  naddcnfass  44355  rfovcnvf1od  44989  dssmapntrcls  45113  dvconstbi  45303  fsumsermpt  46560  icccncfext  46866  voliooicof  46975  etransclem35  47248  rrxsnicc  47279  ovolval4lem1  47628  fcores  48106  1arymaptf1  49723  2arymaptf1  49734  tposideq  49965  fucoid  50425  prcofdiag1  50470  prcofdiag  50471  oppfdiag1  50491  oppfdiag  50493  funcsn  50618  crosspaltd  50935  crossp3d  50936  veronesevrowd  50948