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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ∀wral 3075   Fn wfn 6511  ‘cfv 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-fv 6524

This theorem is referenced by:  foeqcnvco  7279  f1eqcocnv  7280  offveq  7681  tfrlem1  8340  updjudhcoinlf  9884  updjudhcoinrg  9885  ackbij2lem2  10189  ackbij2lem3  10190  fpwwe2lem7  10589  seqfeq2  14032  seqfeq  14034  seqfeq3  14059  ccatlid  14594  ccatrid  14595  ccatass  14596  ccatswrd  14676  swrdccat2  14677  pfxid  14692  ccatpfx  14708  pfxccat1  14709  swrdswrd  14712  cats1un  14728  swrdccatin1  14732  swrdccatin2  14736  pfxccatin12  14740  revccat  14773  revrev  14774  cshco  14843  swrdco  14844  seqshft  15092  seq1st  16596  xpsfeq  17584  yonedainv  18304  pwsco1mhm  18857  ghmquskerco  19315  f1otrspeq  19478  pmtrfinv  19492  symgtrinv  19503  frgpup3lem  19808  ablfac1eu  20106  zrinitorngc  20679  zrtermorngc  20680  zrtermoringc  20712  psgndiflemB  21640  frlmup1  21838  frlmup3  21840  frlmup4  21841  psrlidm  22001  psrridm  22002  psrass1  22003  subrgascl  22107  evlslem1  22123  evlsvvval  22134  psdmplcl  22215  psdvsca  22217  mavmulass  22597  upxp  23671  uptx  23673  cnextfres1  24116  ovolshftlem1  25559  volsup  25606  dvidlem  25965  dvrec  26005  dveq0  26050  dv11cn  26051  ftc1cn  26093  coemulc  26303  aannenlem1  26380  ulmuni  26443  ulmdv  26454  ostthlem1  27679  nvinvfval  30800  sspn  30896  kbass2  32277  xppreima2  32814  fdifsuppconst  32852  indpreima  33004  psgnfzto1stlem  33241  cycpmco2  33274  cyc3co2  33281  ply1gsumz  33756  mplasclco  33774  esplyind  33833  esumcvg  34344  signstres  34830  hgt750lemb  34911  revpfxsfxrev  35427  subfacp1lem4  35494  cvmliftmolem2  35593  msubff1  35867  iprodefisumlem  36051  poimirlem8  38088  poimirlem13  38093  poimirlem14  38094  ftc1cnnc  38152  eqlkr3  39686  cdleme51finvN  41141  sticksstones11  42734  aks6d1c6lem4  42751  ofun  42815  frlmvscadiccat  43089  fiabv  43115  fsuppind  43133  ismrcd2  43241  ofoafo  43894  ofoaid1  43896  ofoaid2  43897  ofoaass  43898  ofoacom  43899  naddcnffo  43902  naddcnfcom  43904  naddcnfid1  43905  naddcnfass  43907  rfovcnvf1od  44541  dssmapntrcls  44665  dvconstbi  44871  fsumsermpt  46116  icccncfext  46422  voliooicof  46531  etransclem35  46804  rrxsnicc  46835  ovolval4lem1  47184  fcores  47622  1arymaptf1  49225  2arymaptf1  49236  tposideq  49470  fucoid  49930  prcofdiag1  49975  prcofdiag  49976  oppfdiag1  49996  oppfdiag  49998  funcsn  50123