Theorem fvmpt2d 6984

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

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

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fv 6522

This theorem is referenced by:  cantnflem1  9649  ghmquskerco  19223  frlmphl  21697  neiptopreu  23027  rrxds  25300  ofoprabco  32595  suppovss  32611  tocycf  33081  elrgspnsubrunlem2  33206  ply1moneq  33562  fedgmullem2  33633  esumcvg  34083  ofcfval2  34101  eulerpartgbij  34370  dstrvprob  34470  itgexpif  34604  hgt750lemb  34654  aks6d1c6lem4  42168  frlmsnic  42535  cvgdvgrat  44309  radcnvrat  44310  binomcxplemnotnn0  44352  fmuldfeqlem1  45587  climreclmpt  45689  climinfmpt  45720  limsupubuzmpt  45724  limsupre2mpt  45735  limsupre3mpt  45739  limsupreuzmpt  45744  liminfvalxrmpt  45791  liminflbuz2  45820  cncficcgt0  45893  dvdivbd  45928  dvnmul  45948  dvnprodlem1  45951  dvnprodlem2  45952  stoweidlem42  46047  dirkeritg  46107  elaa2lem  46238  etransclem4  46243  ioorrnopnxrlem  46311  subsaliuncllem  46362  meaiuninclem  46485  meaiininclem  46491  ovnhoilem1  46606  ovncvr2  46616  ovolval4lem1  46654  iccvonmbllem  46683  vonioolem1  46685  vonioolem2  46686  vonicclem1  46688  vonicclem2  46689  pimconstlt0  46706  pimconstlt1  46707  smfpimltmpt  46751  issmfdmpt  46753  smfaddlem2  46769  smflimlem2  46777  smflimlem4  46779  smfpimgtmpt  46786  smfmullem4  46799  smfpimcclem  46812  smfsuplem1  46816  smfsupmpt  46820  smfinfmpt  46824  smflimsuplem2  46826  smflimsuplem3  46827  smflimsuplem4  46828  fsupdm  46847  finfdm  46851  tposcurf1  49292  fucocolem4  49349