Theorem fvmpt2d 7011

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105   ↦ cmpt 5231  ‘cfv 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fv 6551

This theorem is referenced by:  cantnflem1  9687  frlmphl  21556  neiptopreu  22858  rrxds  25142  ofoprabco  32157  suppovss  32174  tocycf  32547  ghmquskerco  32804  ply1moneq  32940  fedgmullem2  33004  esumcvg  33383  ofcfval2  33401  eulerpartgbij  33670  dstrvprob  33769  itgexpif  33917  hgt750lemb  33967  frlmsnic  41413  cvgdvgrat  43375  radcnvrat  43376  binomcxplemnotnn0  43418  fmuldfeqlem1  44597  climreclmpt  44699  climinfmpt  44730  limsupubuzmpt  44734  limsupre2mpt  44745  limsupre3mpt  44749  limsupreuzmpt  44754  liminfvalxrmpt  44801  liminflbuz2  44830  cncficcgt0  44903  dvdivbd  44938  dvnmul  44958  dvnprodlem1  44961  dvnprodlem2  44962  stoweidlem42  45057  dirkeritg  45117  elaa2lem  45248  etransclem4  45253  ioorrnopnxrlem  45321  subsaliuncllem  45372  meaiuninclem  45495  meaiininclem  45501  ovnhoilem1  45616  ovncvr2  45626  ovolval4lem1  45664  iccvonmbllem  45693  vonioolem1  45695  vonioolem2  45696  vonicclem1  45698  vonicclem2  45699  pimconstlt0  45716  pimconstlt1  45717  smfpimltmpt  45761  issmfdmpt  45763  smfaddlem2  45779  smflimlem2  45787  smflimlem4  45789  smfpimgtmpt  45796  smfmullem4  45809  smfpimcclem  45822  smfsuplem1  45826  smfsupmpt  45830  smfinfmpt  45834  smflimsuplem2  45836  smflimsuplem3  45837  smflimsuplem4  45838  fsupdm  45857  finfdm  45861