Theorem fvmpt2d 7010

Description: Deduction version of fvmpt2 7008. (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 6890	. . 3 ⊢ (𝜑 → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
3	2	adantr 486	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
4		id 23	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
5		fvmpt2d.4	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
6		eqid 2766	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
7	6	fvmpt2 7008	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
8	4, 5, 7	syl2an2 699	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
9	3, 8	eqtrd 2801	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146   ↦ cmpt 5197  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fv 6551

This theorem is used by:  cantnflem1  9668  ghmquskerco  19385  frlmphl  21968  neiptopreu  23327  rrxds  25589  ofoprabco  33046  suppovss  33063  tocycf  33468  elrgspnsubrunlem2  33599  ply1moneq  33909  mplasclco  33937  mplvrpmmhm  33967  fedgmullem2  34051  esumcvg  34507  ofcfval2  34525  eulerpartgbij  34794  dstrvprob  34894  itgexpif  35025  hgt750lemb  35075  aks6d1c6lem4  42981  frlmsnic  43349  cvgdvgrat  45064  radcnvrat  45065  binomcxplemnotnn0  45107  fmuldfeqlem1  46339  climreclmpt  46439  climinfmpt  46470  limsupubuzmpt  46474  limsupre2mpt  46485  limsupre3mpt  46489  limsupreuzmpt  46494  liminfvalxrmpt  46541  liminflbuz2  46570  cncficcgt0  46643  dvdivbd  46678  dvnmul  46698  dvnprodlem1  46701  dvnprodlem2  46702  stoweidlem42  46797  dirkeritg  46857  elaa2lem  46988  etransclem4  46993  ioorrnopnxrlem  47061  subsaliuncllem  47112  meaiuninclem  47235  meaiininclem  47241  ovnhoilem1  47356  ovncvr2  47366  ovolval4lem1  47404  iccvonmbllem  47433  vonioolem1  47435  vonioolem2  47436  vonicclem1  47438  vonicclem2  47439  pimconstlt0  47456  pimconstlt1  47457  smfpimltmpt  47501  issmfdmpt  47503  smfaddlem2  47519  smflimlem2  47527  smflimlem4  47529  smfpimgtmpt  47536  smfmullem4  47549  smfpimcclem  47562  smfsuplem1  47566  smfsupmpt  47570  smfinfmpt  47574  smflimsuplem2  47576  smflimsuplem3  47577  smflimsuplem4  47578  fsupdm  47597  finfdm  47601  tposcurf1  50118  fucocolem4  50175