Theorem eqfnfvd 7026

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 3138	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
3		eqfnfvd.1	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4		eqfnfvd.2	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴)
5		eqfnfv 7023	. . 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 1533   ∈ wcel 2098  ∀wral 3053   Fn wfn 6529  ‘cfv 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pr 5418

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-fv 6542

This theorem is referenced by:  foeqcnvco  7291  f1eqcocnv  7292  f1eqcocnvOLD  7293  offveq  7688  tfrlem1  8372  updjudhcoinlf  9924  updjudhcoinrg  9925  ackbij2lem2  10232  ackbij2lem3  10233  fpwwe2lem7  10629  seqfeq2  13989  seqfeq  13991  seqfeq3  14016  ccatlid  14534  ccatrid  14535  ccatass  14536  ccatswrd  14616  swrdccat2  14617  pfxid  14632  ccatpfx  14649  pfxccat1  14650  swrdswrd  14653  cats1un  14669  swrdccatin1  14673  swrdccatin2  14677  pfxccatin12  14681  revccat  14714  revrev  14715  cshco  14785  swrdco  14786  seqshft  15030  seq1st  16507  xpsfeq  17510  yonedainv  18238  pwsco1mhm  18749  f1otrspeq  19359  pmtrfinv  19373  symgtrinv  19384  frgpup3lem  19689  ablfac1eu  19987  zrinitorngc  20530  zrtermorngc  20531  zrtermoringc  20563  psgndiflemB  21463  frlmup1  21663  frlmup3  21665  frlmup4  21666  psrlidm  21835  psrridm  21836  psrass1  21837  subrgascl  21939  evlslem1  21957  psdmplcl  22015  psdvsca  22017  mavmulass  22375  upxp  23451  uptx  23453  cnextfres1  23896  ovolshftlem1  25362  volsup  25409  dvidlem  25768  dvrec  25811  dveq0  25857  dv11cn  25858  ftc1cn  25902  coemulc  26111  aannenlem1  26184  ulmuni  26247  ulmdv  26258  ostthlem1  27479  nvinvfval  30365  sspn  30461  kbass2  31842  xppreima2  32348  fdifsuppconst  32383  psgnfzto1stlem  32730  cycpmco2  32763  cyc3co2  32770  ghmquskerco  33001  ply1gsumz  33138  indpreima  33515  esumcvg  33576  signstres  34078  hgt750lemb  34159  revpfxsfxrev  34597  subfacp1lem4  34665  cvmliftmolem2  34764  msubff1  35038  iprodefisumlem  35206  poimirlem8  36990  poimirlem13  36995  poimirlem14  36996  ftc1cnnc  37054  eqlkr3  38465  cdleme51finvN  39921  sticksstones11  41469  metakunt33  41514  ofun  41555  frlmvscadiccat  41577  evlsvvval  41628  fsuppind  41655  ismrcd2  41951  ofoafo  42620  ofoaid1  42622  ofoaid2  42623  ofoaass  42624  ofoacom  42625  naddcnffo  42628  naddcnfcom  42630  naddcnfid1  42631  naddcnfass  42633  rfovcnvf1od  43269  dssmapntrcls  43393  dvconstbi  43607  fsumsermpt  44805  icccncfext  45113  voliooicof  45222  etransclem35  45495  rrxsnicc  45526  ovolval4lem1  45875  fcores  46287  1arymaptf1  47541  2arymaptf1  47552