Theorem fvmpt2d 6961

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

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

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fv 6506

This theorem is referenced by:  cantnflem1  9610  ghmquskerco  19259  frlmphl  21761  neiptopreu  23098  rrxds  25360  ofoprabco  32737  suppovss  32754  tocycf  33178  elrgspnsubrunlem2  33309  ply1moneq  33648  mplvrpmmhm  33690  fedgmullem2  33774  esumcvg  34230  ofcfval2  34248  eulerpartgbij  34516  dstrvprob  34616  itgexpif  34750  hgt750lemb  34800  aks6d1c6lem4  42612  frlmsnic  42985  cvgdvgrat  44740  radcnvrat  44741  binomcxplemnotnn0  44783  fmuldfeqlem1  46012  climreclmpt  46112  climinfmpt  46143  limsupubuzmpt  46147  limsupre2mpt  46158  limsupre3mpt  46162  limsupreuzmpt  46167  liminfvalxrmpt  46214  liminflbuz2  46243  cncficcgt0  46316  dvdivbd  46351  dvnmul  46371  dvnprodlem1  46374  dvnprodlem2  46375  stoweidlem42  46470  dirkeritg  46530  elaa2lem  46661  etransclem4  46666  ioorrnopnxrlem  46734  subsaliuncllem  46785  meaiuninclem  46908  meaiininclem  46914  ovnhoilem1  47029  ovncvr2  47039  ovolval4lem1  47077  iccvonmbllem  47106  vonioolem1  47108  vonioolem2  47109  vonicclem1  47111  vonicclem2  47112  pimconstlt0  47129  pimconstlt1  47130  smfpimltmpt  47174  issmfdmpt  47176  smfaddlem2  47192  smflimlem2  47200  smflimlem4  47202  smfpimgtmpt  47209  smfmullem4  47222  smfpimcclem  47235  smfsuplem1  47239  smfsupmpt  47243  smfinfmpt  47247  smflimsuplem2  47249  smflimsuplem3  47250  smflimsuplem4  47251  fsupdm  47270  finfdm  47274  tposcurf1  49774  fucocolem4  49831