Theorem fvmpt2d 6890

Description: Deduction version of fvmpt2 6888. (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 6778	. . 3 ⊢ (𝜑 → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
3	2	adantr 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
4		id 22	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
5		fvmpt2d.4	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
6		eqid 2738	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
7	6	fvmpt2 6888	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
8	4, 5, 7	syl2an2 683	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
9	3, 8	eqtrd 2778	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106   ↦ cmpt 5159  ‘cfv 6435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5225  ax-nul 5232  ax-pr 5354

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3433  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5077  df-opab 5139  df-mpt 5160  df-id 5491  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-iota 6393  df-fun 6437  df-fv 6443

This theorem is referenced by:  cantnflem1  9445  frlmphl  20986  neiptopreu  22282  rrxds  24555  ofoprabco  30998  suppovss  31014  tocycf  31381  fedgmullem2  31708  esumcvg  32051  ofcfval2  32069  eulerpartgbij  32336  dstrvprob  32435  itgexpif  32583  hgt750lemb  32633  frlmsnic  40260  cvgdvgrat  41901  radcnvrat  41902  binomcxplemnotnn0  41944  fmuldfeqlem1  43093  climreclmpt  43195  climinfmpt  43226  limsupubuzmpt  43230  limsupre2mpt  43241  limsupre3mpt  43245  limsupreuzmpt  43250  liminfvalxrmpt  43297  liminflbuz2  43326  cncficcgt0  43399  dvdivbd  43434  dvnmul  43454  dvnprodlem1  43457  dvnprodlem2  43458  stoweidlem42  43553  dirkeritg  43613  elaa2lem  43744  etransclem4  43749  ioorrnopnxrlem  43817  subsaliuncllem  43866  meaiuninclem  43988  meaiininclem  43994  ovnhoilem1  44109  ovncvr2  44119  ovolval4lem1  44157  iccvonmbllem  44186  vonioolem1  44188  vonioolem2  44189  vonicclem1  44191  vonicclem2  44192  pimconstlt0  44208  pimconstlt1  44209  pimgtmnf  44226  smfpimltmpt  44249  issmfdmpt  44251  smfpimltxrmpt  44261  smfaddlem2  44266  smflimlem2  44274  smflimlem4  44276  smfpimgtmpt  44283  smfpimgtxrmpt  44286  smfmullem4  44295  smfpimcclem  44307  smfsuplem1  44311  smfsupmpt  44315  smfinfmpt  44319  smflimsuplem2  44321  smflimsuplem3  44322  smflimsuplem4  44323