Theorem fvmpt2d 6963

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5181  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fv 6508

This theorem is referenced by:  cantnflem1  9610  ghmquskerco  19225  frlmphl  21748  neiptopreu  23089  rrxds  25361  ofoprabco  32753  suppovss  32770  tocycf  33210  elrgspnsubrunlem2  33341  ply1moneq  33680  mplvrpmmhm  33722  fedgmullem2  33807  esumcvg  34263  ofcfval2  34281  eulerpartgbij  34549  dstrvprob  34649  itgexpif  34783  hgt750lemb  34833  aks6d1c6lem4  42537  frlmsnic  42904  cvgdvgrat  44663  radcnvrat  44664  binomcxplemnotnn0  44706  fmuldfeqlem1  45936  climreclmpt  46036  climinfmpt  46067  limsupubuzmpt  46071  limsupre2mpt  46082  limsupre3mpt  46086  limsupreuzmpt  46091  liminfvalxrmpt  46138  liminflbuz2  46167  cncficcgt0  46240  dvdivbd  46275  dvnmul  46295  dvnprodlem1  46298  dvnprodlem2  46299  stoweidlem42  46394  dirkeritg  46454  elaa2lem  46585  etransclem4  46590  ioorrnopnxrlem  46658  subsaliuncllem  46709  meaiuninclem  46832  meaiininclem  46838  ovnhoilem1  46953  ovncvr2  46963  ovolval4lem1  47001  iccvonmbllem  47030  vonioolem1  47032  vonioolem2  47033  vonicclem1  47035  vonicclem2  47036  pimconstlt0  47053  pimconstlt1  47054  smfpimltmpt  47098  issmfdmpt  47100  smfaddlem2  47116  smflimlem2  47124  smflimlem4  47126  smfpimgtmpt  47133  smfmullem4  47146  smfpimcclem  47159  smfsuplem1  47163  smfsupmpt  47167  smfinfmpt  47171  smflimsuplem2  47173  smflimsuplem3  47174  smflimsuplem4  47175  fsupdm  47194  finfdm  47198  tposcurf1  49652  fucocolem4  49709