Theorem fvmpt2d 6781

Description: Deduction version of fvmpt2 6779. (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 6672	. . 3 ⊢ (𝜑 → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
3	2	adantr 483	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
4		id 22	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
5		fvmpt2d.4	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
6		eqid 2821	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
7	6	fvmpt2 6779	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
8	4, 5, 7	syl2an2 684	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
9	3, 8	eqtrd 2856	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ↦ cmpt 5146  ‘cfv 6355

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fv 6363

This theorem is referenced by:  cantnflem1  9152  frlmphl  20925  neiptopreu  21741  rrxds  23996  ofoprabco  30409  suppovss  30426  tocycf  30759  fedgmullem2  31026  esumcvg  31345  ofcfval2  31363  eulerpartgbij  31630  dstrvprob  31729  itgexpif  31877  hgt750lemb  31927  frlmsnic  39198  cvgdvgrat  40694  radcnvrat  40695  binomcxplemnotnn0  40737  fmuldfeqlem1  41912  climreclmpt  42014  climinfmpt  42045  limsupubuzmpt  42049  limsupre2mpt  42060  limsupre3mpt  42064  limsupreuzmpt  42069  liminfvalxrmpt  42116  liminflbuz2  42145  cncficcgt0  42220  dvdivbd  42257  dvnmul  42277  dvnprodlem1  42280  dvnprodlem2  42281  stoweidlem42  42376  dirkeritg  42436  elaa2lem  42567  etransclem4  42572  ioorrnopnxrlem  42640  subsaliuncllem  42689  meaiuninclem  42811  meaiininclem  42817  ovnhoilem1  42932  ovncvr2  42942  ovolval4lem1  42980  iccvonmbllem  43009  vonioolem1  43011  vonioolem2  43012  vonicclem1  43014  vonicclem2  43015  pimconstlt0  43031  pimconstlt1  43032  pimgtmnf  43049  smfpimltmpt  43072  issmfdmpt  43074  smfpimltxrmpt  43084  smfaddlem2  43089  smflimlem2  43097  smflimlem4  43099  smfpimgtmpt  43106  smfpimgtxrmpt  43109  smfmullem4  43118  smfpimcclem  43130  smfsuplem1  43134  smfsupmpt  43138  smfinfmpt  43142  smflimsuplem2  43144  smflimsuplem3  43145  smflimsuplem4  43146