Theorem eqfnfvd 7009

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 3126	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
3		eqfnfvd.1	. . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4		eqfnfvd.2	. . 3 ⊢ (𝜑 → 𝐺 Fn 𝐴)
5		eqfnfv 7006	. . 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 2109  ∀wral 3045   Fn wfn 6509  ‘cfv 6514

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-fv 6522

This theorem is referenced by:  foeqcnvco  7278  f1eqcocnv  7279  offveq  7682  tfrlem1  8347  updjudhcoinlf  9892  updjudhcoinrg  9893  ackbij2lem2  10199  ackbij2lem3  10200  fpwwe2lem7  10597  seqfeq2  13997  seqfeq  13999  seqfeq3  14024  ccatlid  14558  ccatrid  14559  ccatass  14560  ccatswrd  14640  swrdccat2  14641  pfxid  14656  ccatpfx  14673  pfxccat1  14674  swrdswrd  14677  cats1un  14693  swrdccatin1  14697  swrdccatin2  14701  pfxccatin12  14705  revccat  14738  revrev  14739  cshco  14809  swrdco  14810  seqshft  15058  seq1st  16548  xpsfeq  17533  yonedainv  18249  pwsco1mhm  18766  ghmquskerco  19223  f1otrspeq  19384  pmtrfinv  19398  symgtrinv  19409  frgpup3lem  19714  ablfac1eu  20012  zrinitorngc  20558  zrtermorngc  20559  zrtermoringc  20591  psgndiflemB  21516  frlmup1  21714  frlmup3  21716  frlmup4  21717  psrlidm  21878  psrridm  21879  psrass1  21880  subrgascl  21980  evlslem1  21996  psdmplcl  22056  psdvsca  22058  mavmulass  22443  upxp  23517  uptx  23519  cnextfres1  23962  ovolshftlem1  25417  volsup  25464  dvidlem  25823  dvrec  25866  dveq0  25912  dv11cn  25913  ftc1cn  25957  coemulc  26167  aannenlem1  26243  ulmuni  26308  ulmdv  26319  ostthlem1  27545  nvinvfval  30576  sspn  30672  kbass2  32053  xppreima2  32582  fdifsuppconst  32619  indpreima  32795  psgnfzto1stlem  33064  cycpmco2  33097  cyc3co2  33104  ply1gsumz  33571  esumcvg  34083  signstres  34573  hgt750lemb  34654  revpfxsfxrev  35110  subfacp1lem4  35177  cvmliftmolem2  35276  msubff1  35550  iprodefisumlem  35734  poimirlem8  37629  poimirlem13  37634  poimirlem14  37635  ftc1cnnc  37693  eqlkr3  39101  cdleme51finvN  40557  sticksstones11  42151  aks6d1c6lem4  42168  ofun  42231  frlmvscadiccat  42501  fiabv  42531  evlsvvval  42558  fsuppind  42585  ismrcd2  42694  ofoafo  43352  ofoaid1  43354  ofoaid2  43355  ofoaass  43356  ofoacom  43357  naddcnffo  43360  naddcnfcom  43362  naddcnfid1  43363  naddcnfass  43365  rfovcnvf1od  44000  dssmapntrcls  44124  dvconstbi  44330  fsumsermpt  45584  icccncfext  45892  voliooicof  46001  etransclem35  46274  rrxsnicc  46305  ovolval4lem1  46654  fcores  47072  1arymaptf1  48635  2arymaptf1  48646  tposideq  48880  fucoid  49341  prcofdiag1  49386  prcofdiag  49387  oppfdiag1  49407  oppfdiag  49409  funcsn  49534