Theorem eqfnfvd 7024

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3051   Fn wfn 6526  ‘cfv 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-fv 6539

This theorem is referenced by:  foeqcnvco  7293  f1eqcocnv  7294  offveq  7697  tfrlem1  8390  updjudhcoinlf  9946  updjudhcoinrg  9947  ackbij2lem2  10253  ackbij2lem3  10254  fpwwe2lem7  10651  seqfeq2  14043  seqfeq  14045  seqfeq3  14070  ccatlid  14604  ccatrid  14605  ccatass  14606  ccatswrd  14686  swrdccat2  14687  pfxid  14702  ccatpfx  14719  pfxccat1  14720  swrdswrd  14723  cats1un  14739  swrdccatin1  14743  swrdccatin2  14747  pfxccatin12  14751  revccat  14784  revrev  14785  cshco  14855  swrdco  14856  seqshft  15104  seq1st  16590  xpsfeq  17577  yonedainv  18293  pwsco1mhm  18810  ghmquskerco  19267  f1otrspeq  19428  pmtrfinv  19442  symgtrinv  19453  frgpup3lem  19758  ablfac1eu  20056  zrinitorngc  20602  zrtermorngc  20603  zrtermoringc  20635  psgndiflemB  21560  frlmup1  21758  frlmup3  21760  frlmup4  21761  psrlidm  21922  psrridm  21923  psrass1  21924  subrgascl  22024  evlslem1  22040  psdmplcl  22100  psdvsca  22102  mavmulass  22487  upxp  23561  uptx  23563  cnextfres1  24006  ovolshftlem1  25462  volsup  25509  dvidlem  25868  dvrec  25911  dveq0  25957  dv11cn  25958  ftc1cn  26002  coemulc  26212  aannenlem1  26288  ulmuni  26353  ulmdv  26364  ostthlem1  27590  nvinvfval  30621  sspn  30717  kbass2  32098  xppreima2  32629  fdifsuppconst  32666  indpreima  32842  psgnfzto1stlem  33111  cycpmco2  33144  cyc3co2  33151  ply1gsumz  33608  esumcvg  34117  signstres  34607  hgt750lemb  34688  revpfxsfxrev  35138  subfacp1lem4  35205  cvmliftmolem2  35304  msubff1  35578  iprodefisumlem  35757  poimirlem8  37652  poimirlem13  37657  poimirlem14  37658  ftc1cnnc  37716  eqlkr3  39119  cdleme51finvN  40575  sticksstones11  42169  aks6d1c6lem4  42186  metakunt33  42250  ofun  42287  frlmvscadiccat  42529  fiabv  42559  evlsvvval  42586  fsuppind  42613  ismrcd2  42722  ofoafo  43380  ofoaid1  43382  ofoaid2  43383  ofoaass  43384  ofoacom  43385  naddcnffo  43388  naddcnfcom  43390  naddcnfid1  43391  naddcnfass  43393  rfovcnvf1od  44028  dssmapntrcls  44152  dvconstbi  44358  fsumsermpt  45608  icccncfext  45916  voliooicof  46025  etransclem35  46298  rrxsnicc  46329  ovolval4lem1  46678  fcores  47096  1arymaptf1  48622  2arymaptf1  48633  tposideq  48863  fucoid  49259