Theorem fvmpt2d 6985

Description: Deduction version of fvmpt2 6983. (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 6865	. . 3 ⊢ (𝜑 → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
3	2	adantr 484	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
4		id 22	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
5		fvmpt2d.4	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
6		eqid 2761	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
7	6	fvmpt2 6983	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
8	4, 5, 7	syl2an2 696	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
9	3, 8	eqtrd 2796	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ↦ cmpt 5180  ‘cfv 6517

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 5245  ax-nul 5255  ax-pr 5389

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 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fv 6525

This theorem is referenced by:  cantnflem1  9641  ghmquskerco  19307  frlmphl  21813  neiptopreu  23173  rrxds  25435  ofoprabco  32816  suppovss  32833  tocycf  33258  elrgspnsubrunlem2  33390  ply1moneq  33745  mplasclco  33774  mplvrpmmhm  33804  fedgmullem2  33888  esumcvg  34344  ofcfval2  34362  eulerpartgbij  34630  dstrvprob  34730  itgexpif  34864  hgt750lemb  34914  aks6d1c6lem4  42754  frlmsnic  43122  cvgdvgrat  44853  radcnvrat  44854  binomcxplemnotnn0  44896  fmuldfeqlem1  46122  climreclmpt  46222  climinfmpt  46253  limsupubuzmpt  46257  limsupre2mpt  46268  limsupre3mpt  46272  limsupreuzmpt  46277  liminfvalxrmpt  46324  liminflbuz2  46353  cncficcgt0  46426  dvdivbd  46461  dvnmul  46481  dvnprodlem1  46484  dvnprodlem2  46485  stoweidlem42  46580  dirkeritg  46640  elaa2lem  46771  etransclem4  46776  ioorrnopnxrlem  46844  subsaliuncllem  46895  meaiuninclem  47018  meaiininclem  47024  ovnhoilem1  47139  ovncvr2  47149  ovolval4lem1  47187  iccvonmbllem  47216  vonioolem1  47218  vonioolem2  47219  vonicclem1  47221  vonicclem2  47222  pimconstlt0  47239  pimconstlt1  47240  smfpimltmpt  47284  issmfdmpt  47286  smfaddlem2  47302  smflimlem2  47310  smflimlem4  47312  smfpimgtmpt  47319  smfmullem4  47332  smfpimcclem  47345  smfsuplem1  47349  smfsupmpt  47353  smfinfmpt  47357  smflimsuplem2  47359  smflimsuplem3  47360  smflimsuplem4  47361  fsupdm  47380  finfdm  47384  tposcurf1  49884  fucocolem4  49941