Theorem fvmpt2d 6954

Description: Deduction version of fvmpt2 6952. (Contributed by Thierry Arnoux, 8-Dec-2016.)

Hypotheses

Ref	Expression
fvmpt2d.1	⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
fvmpt2d.4	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)

Assertion

Ref	Expression
fvmpt2d	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fvmpt2d

Step	Hyp	Ref	Expression
1		fvmpt2d.1	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))
2	1	fveq1d 6836	. . 3 ⊢ (𝜑 → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
3	2	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
4		id 22	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
5		fvmpt2d.4	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
6		eqid 2736	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
7	6	fvmpt2 6952	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
8	4, 5, 7	syl2an2 686	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
9	3, 8	eqtrd 2771	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5179  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  cantnflem1  9598  ghmquskerco  19213  frlmphl  21736  neiptopreu  23077  rrxds  25349  ofoprabco  32742  suppovss  32760  tocycf  33199  elrgspnsubrunlem2  33330  ply1moneq  33669  mplvrpmmhm  33711  fedgmullem2  33787  esumcvg  34243  ofcfval2  34261  eulerpartgbij  34529  dstrvprob  34629  itgexpif  34763  hgt750lemb  34813  aks6d1c6lem4  42423  frlmsnic  42791  cvgdvgrat  44550  radcnvrat  44551  binomcxplemnotnn0  44593  fmuldfeqlem1  45824  climreclmpt  45924  climinfmpt  45955  limsupubuzmpt  45959  limsupre2mpt  45970  limsupre3mpt  45974  limsupreuzmpt  45979  liminfvalxrmpt  46026  liminflbuz2  46055  cncficcgt0  46128  dvdivbd  46163  dvnmul  46183  dvnprodlem1  46186  dvnprodlem2  46187  stoweidlem42  46282  dirkeritg  46342  elaa2lem  46473  etransclem4  46478  ioorrnopnxrlem  46546  subsaliuncllem  46597  meaiuninclem  46720  meaiininclem  46726  ovnhoilem1  46841  ovncvr2  46851  ovolval4lem1  46889  iccvonmbllem  46918  vonioolem1  46920  vonioolem2  46921  vonicclem1  46923  vonicclem2  46924  pimconstlt0  46941  pimconstlt1  46942  smfpimltmpt  46986  issmfdmpt  46988  smfaddlem2  47004  smflimlem2  47012  smflimlem4  47014  smfpimgtmpt  47021  smfmullem4  47034  smfpimcclem  47047  smfsuplem1  47051  smfsupmpt  47055  smfinfmpt  47059  smflimsuplem2  47061  smflimsuplem3  47062  smflimsuplem4  47063  fsupdm  47082  finfdm  47086  tposcurf1  49540  fucocolem4  49597