Theorem fvmpt2d 6981

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5188  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fv 6519

This theorem is referenced by:  cantnflem1  9642  ghmquskerco  19216  frlmphl  21690  neiptopreu  23020  rrxds  25293  ofoprabco  32588  suppovss  32604  tocycf  33074  elrgspnsubrunlem2  33199  ply1moneq  33555  fedgmullem2  33626  esumcvg  34076  ofcfval2  34094  eulerpartgbij  34363  dstrvprob  34463  itgexpif  34597  hgt750lemb  34647  aks6d1c6lem4  42161  frlmsnic  42528  cvgdvgrat  44302  radcnvrat  44303  binomcxplemnotnn0  44345  fmuldfeqlem1  45580  climreclmpt  45682  climinfmpt  45713  limsupubuzmpt  45717  limsupre2mpt  45728  limsupre3mpt  45732  limsupreuzmpt  45737  liminfvalxrmpt  45784  liminflbuz2  45813  cncficcgt0  45886  dvdivbd  45921  dvnmul  45941  dvnprodlem1  45944  dvnprodlem2  45945  stoweidlem42  46040  dirkeritg  46100  elaa2lem  46231  etransclem4  46236  ioorrnopnxrlem  46304  subsaliuncllem  46355  meaiuninclem  46478  meaiininclem  46484  ovnhoilem1  46599  ovncvr2  46609  ovolval4lem1  46647  iccvonmbllem  46676  vonioolem1  46678  vonioolem2  46679  vonicclem1  46681  vonicclem2  46682  pimconstlt0  46699  pimconstlt1  46700  smfpimltmpt  46744  issmfdmpt  46746  smfaddlem2  46762  smflimlem2  46770  smflimlem4  46772  smfpimgtmpt  46779  smfmullem4  46792  smfpimcclem  46805  smfsuplem1  46809  smfsupmpt  46813  smfinfmpt  46817  smflimsuplem2  46819  smflimsuplem3  46820  smflimsuplem4  46821  fsupdm  46840  finfdm  46844  tposcurf1  49288  fucocolem4  49345