Theorem eqfnfvd 7043

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099  ∀wral 3058   Fn wfn 6543  ‘cfv 6548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-fv 6556

This theorem is referenced by:  foeqcnvco  7309  f1eqcocnv  7310  f1eqcocnvOLD  7311  offveq  7709  tfrlem1  8396  updjudhcoinlf  9955  updjudhcoinrg  9956  ackbij2lem2  10263  ackbij2lem3  10264  fpwwe2lem7  10660  seqfeq2  14022  seqfeq  14024  seqfeq3  14049  ccatlid  14568  ccatrid  14569  ccatass  14570  ccatswrd  14650  swrdccat2  14651  pfxid  14666  ccatpfx  14683  pfxccat1  14684  swrdswrd  14687  cats1un  14703  swrdccatin1  14707  swrdccatin2  14711  pfxccatin12  14715  revccat  14748  revrev  14749  cshco  14819  swrdco  14820  seqshft  15064  seq1st  16541  xpsfeq  17544  yonedainv  18272  pwsco1mhm  18783  ghmquskerco  19234  f1otrspeq  19401  pmtrfinv  19415  symgtrinv  19426  frgpup3lem  19731  ablfac1eu  20029  zrinitorngc  20574  zrtermorngc  20575  zrtermoringc  20607  psgndiflemB  21531  frlmup1  21731  frlmup3  21733  frlmup4  21734  psrlidm  21904  psrridm  21905  psrass1  21906  subrgascl  22009  evlslem1  22027  psdmplcl  22085  psdvsca  22087  mavmulass  22450  upxp  23526  uptx  23528  cnextfres1  23971  ovolshftlem1  25437  volsup  25484  dvidlem  25843  dvrec  25886  dveq0  25932  dv11cn  25933  ftc1cn  25977  coemulc  26188  aannenlem1  26262  ulmuni  26327  ulmdv  26338  ostthlem1  27559  nvinvfval  30449  sspn  30545  kbass2  31926  xppreima2  32436  fdifsuppconst  32469  psgnfzto1stlem  32821  cycpmco2  32854  cyc3co2  32861  ply1gsumz  33265  indpreima  33644  esumcvg  33705  signstres  34207  hgt750lemb  34288  revpfxsfxrev  34725  subfacp1lem4  34793  cvmliftmolem2  34892  msubff1  35166  iprodefisumlem  35334  poimirlem8  37101  poimirlem13  37106  poimirlem14  37107  ftc1cnnc  37165  eqlkr3  38573  cdleme51finvN  40029  sticksstones11  41628  aks6d1c6lem4  41645  metakunt33  41689  ofun  41727  frlmvscadiccat  41746  evlsvvval  41796  fsuppind  41823  ismrcd2  42119  ofoafo  42785  ofoaid1  42787  ofoaid2  42788  ofoaass  42789  ofoacom  42790  naddcnffo  42793  naddcnfcom  42795  naddcnfid1  42796  naddcnfass  42798  rfovcnvf1od  43434  dssmapntrcls  43558  dvconstbi  43771  fsumsermpt  44967  icccncfext  45275  voliooicof  45384  etransclem35  45657  rrxsnicc  45688  ovolval4lem1  46037  fcores  46449  1arymaptf1  47715  2arymaptf1  47726

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »