Theorem eqfnfvd 7034

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  ∀wral 3059   Fn wfn 6537  ‘cfv 6542

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-fv 6550

This theorem is referenced by:  foeqcnvco  7300  f1eqcocnv  7301  f1eqcocnvOLD  7302  offveq  7696  tfrlem1  8378  updjudhcoinlf  9929  updjudhcoinrg  9930  ackbij2lem2  10237  ackbij2lem3  10238  fpwwe2lem7  10634  seqfeq2  13995  seqfeq  13997  seqfeq3  14022  ccatlid  14540  ccatrid  14541  ccatass  14542  ccatswrd  14622  swrdccat2  14623  pfxid  14638  ccatpfx  14655  pfxccat1  14656  swrdswrd  14659  cats1un  14675  swrdccatin1  14679  swrdccatin2  14683  pfxccatin12  14687  revccat  14720  revrev  14721  cshco  14791  swrdco  14792  seqshft  15036  seq1st  16512  xpsfeq  17513  yonedainv  18238  pwsco1mhm  18749  f1otrspeq  19356  pmtrfinv  19370  symgtrinv  19381  frgpup3lem  19686  ablfac1eu  19984  psgndiflemB  21372  frlmup1  21572  frlmup3  21574  frlmup4  21575  psrlidm  21742  psrridm  21743  psrass1  21744  subrgascl  21846  evlslem1  21864  mavmulass  22271  upxp  23347  uptx  23349  cnextfres1  23792  ovolshftlem1  25258  volsup  25305  dvidlem  25664  dvrec  25707  dveq0  25752  dv11cn  25753  ftc1cn  25795  coemulc  26004  aannenlem1  26077  ulmuni  26140  ulmdv  26151  ostthlem1  27366  nvinvfval  30160  sspn  30256  kbass2  31637  xppreima2  32143  fdifsuppconst  32178  psgnfzto1stlem  32529  cycpmco2  32562  cyc3co2  32569  ghmquskerco  32803  ply1gsumz  32944  indpreima  33321  esumcvg  33382  signstres  33884  hgt750lemb  33966  revpfxsfxrev  34404  subfacp1lem4  34472  cvmliftmolem2  34571  msubff1  34845  iprodefisumlem  35014  poimirlem8  36799  poimirlem13  36804  poimirlem14  36805  ftc1cnnc  36863  eqlkr3  38274  cdleme51finvN  39730  sticksstones11  41278  metakunt33  41323  ofun  41364  frlmvscadiccat  41386  evlsvvval  41437  fsuppind  41464  ismrcd2  41739  ofoafo  42408  ofoaid1  42410  ofoaid2  42411  ofoaass  42412  ofoacom  42413  naddcnffo  42416  naddcnfcom  42418  naddcnfid1  42419  naddcnfass  42421  rfovcnvf1od  43057  dssmapntrcls  43181  dvconstbi  43395  fsumsermpt  44593  icccncfext  44901  voliooicof  45010  etransclem35  45283  rrxsnicc  45314  ovolval4lem1  45663  fcores  46075  zrinitorngc  46986  zrtermorngc  46987  zrtermoringc  47056  1arymaptf1  47415  2arymaptf1  47426