Theorem fvmpt2d 7004

Description: Deduction version of fvmpt2 7002. (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 6884	. . 3 ⊢ (𝜑 → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
3	2	adantr 485	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
4		id 23	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
5		fvmpt2d.4	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
6		eqid 2769	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
7	6	fvmpt2 7002	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
8	4, 5, 7	syl2an2 698	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
9	3, 8	eqtrd 2804	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149   ↦ cmpt 5196  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is referenced by:  cantnflem1  9657  ghmquskerco  19353  frlmphl  21899  neiptopreu  23258  rrxds  25520  ofoprabco  32949  suppovss  32966  tocycf  33377  elrgspnsubrunlem2  33508  ply1moneq  33822  mplasclco  33850  mplvrpmmhm  33880  fedgmullem2  33964  esumcvg  34420  ofcfval2  34438  eulerpartgbij  34706  dstrvprob  34806  itgexpif  34937  hgt750lemb  34987  aks6d1c6lem4  42829  frlmsnic  43199  cvgdvgrat  44914  radcnvrat  44915  binomcxplemnotnn0  44957  fmuldfeqlem1  46189  climreclmpt  46289  climinfmpt  46320  limsupubuzmpt  46324  limsupre2mpt  46335  limsupre3mpt  46339  limsupreuzmpt  46344  liminfvalxrmpt  46391  liminflbuz2  46420  cncficcgt0  46493  dvdivbd  46528  dvnmul  46548  dvnprodlem1  46551  dvnprodlem2  46552  stoweidlem42  46647  dirkeritg  46707  elaa2lem  46838  etransclem4  46843  ioorrnopnxrlem  46911  subsaliuncllem  46962  meaiuninclem  47085  meaiininclem  47091  ovnhoilem1  47206  ovncvr2  47216  ovolval4lem1  47254  iccvonmbllem  47283  vonioolem1  47285  vonioolem2  47286  vonicclem1  47288  vonicclem2  47289  pimconstlt0  47306  pimconstlt1  47307  smfpimltmpt  47351  issmfdmpt  47353  smfaddlem2  47369  smflimlem2  47377  smflimlem4  47379  smfpimgtmpt  47386  smfmullem4  47399  smfpimcclem  47412  smfsuplem1  47416  smfsupmpt  47420  smfinfmpt  47424  smflimsuplem2  47426  smflimsuplem3  47427  smflimsuplem4  47428  fsupdm  47447  finfdm  47451  tposcurf1  49961  fucocolem4  50018