Theorem fvmpt2d 6942

Description: Deduction version of fvmpt2 6940. (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 6824	. . 3 ⊢ (𝜑 → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
3	2	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
4		id 22	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
5		fvmpt2d.4	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
6		eqid 2731	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
7	6	fvmpt2 6940	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
8	4, 5, 7	syl2an2 686	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
9	3, 8	eqtrd 2766	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111   ↦ cmpt 5170  ‘cfv 6481

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fv 6489

This theorem is referenced by:  cantnflem1  9579  ghmquskerco  19196  frlmphl  21718  neiptopreu  23048  rrxds  25320  ofoprabco  32646  suppovss  32662  tocycf  33086  elrgspnsubrunlem2  33215  ply1moneq  33550  mplvrpmmhm  33576  fedgmullem2  33643  esumcvg  34099  ofcfval2  34117  eulerpartgbij  34385  dstrvprob  34485  itgexpif  34619  hgt750lemb  34669  aks6d1c6lem4  42265  frlmsnic  42632  cvgdvgrat  44405  radcnvrat  44406  binomcxplemnotnn0  44448  fmuldfeqlem1  45681  climreclmpt  45781  climinfmpt  45812  limsupubuzmpt  45816  limsupre2mpt  45827  limsupre3mpt  45831  limsupreuzmpt  45836  liminfvalxrmpt  45883  liminflbuz2  45912  cncficcgt0  45985  dvdivbd  46020  dvnmul  46040  dvnprodlem1  46043  dvnprodlem2  46044  stoweidlem42  46139  dirkeritg  46199  elaa2lem  46330  etransclem4  46335  ioorrnopnxrlem  46403  subsaliuncllem  46454  meaiuninclem  46577  meaiininclem  46583  ovnhoilem1  46698  ovncvr2  46708  ovolval4lem1  46746  iccvonmbllem  46775  vonioolem1  46777  vonioolem2  46778  vonicclem1  46780  vonicclem2  46781  pimconstlt0  46798  pimconstlt1  46799  smfpimltmpt  46843  issmfdmpt  46845  smfaddlem2  46861  smflimlem2  46869  smflimlem4  46871  smfpimgtmpt  46878  smfmullem4  46891  smfpimcclem  46904  smfsuplem1  46908  smfsupmpt  46912  smfinfmpt  46916  smflimsuplem2  46918  smflimsuplem3  46919  smflimsuplem4  46920  fsupdm  46939  finfdm  46943  tposcurf1  49399  fucocolem4  49456