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 486	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))
4		id 23	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
5		fvmpt2d.4	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
6		eqid 2762	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
7	6	fvmpt2 7002	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
8	4, 5, 7	syl2an2 699	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
9	3, 8	eqtrd 2797	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5190  ‘cfv 6537

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is used by:  cantnflem1  9672  ghmquskerco  19417  frlmphl  22000  neiptopreu  23364  rrxds  25627  ofoprabco  33145  suppovss  33161  tocycf  33565  elrgspnsubrunlem2  33696  ply1moneq  34006  mplasclco  34034  mplvrpmmhm  34064  fedgmullem2  34148  esumcvg  34604  ofcfval2  34622  eulerpartgbij  34891  dstrvprob  34991  itgexpif  35122  hgt750lemb  35172  aks6d1c6lem4  43047  frlmsnic  43430  cvgdvgrat  45145  radcnvrat  45146  binomcxplemnotnn0  45188  fmuldfeqlem1  46420  climreclmpt  46520  climinfmpt  46551  limsupubuzmpt  46555  limsupre2mpt  46566  limsupre3mpt  46570  limsupreuzmpt  46575  liminfvalxrmpt  46622  liminflbuz2  46651  cncficcgt0  46724  dvdivbd  46759  dvnmul  46779  dvnprodlem1  46782  dvnprodlem2  46783  stoweidlem42  46878  dirkeritg  46938  elaa2lem  47069  etransclem4  47074  ioorrnopnxrlem  47142  subsaliuncllem  47193  meaiuninclem  47316  meaiininclem  47322  ovnhoilem1  47437  ovncvr2  47447  ovolval4lem1  47485  iccvonmbllem  47514  vonioolem1  47516  vonioolem2  47517  vonicclem1  47519  vonicclem2  47520  pimconstlt0  47537  pimconstlt1  47538  smfpimltmpt  47582  issmfdmpt  47584  smfaddlem2  47600  smflimlem2  47608  smflimlem4  47610  smfpimgtmpt  47617  smfmullem4  47630  smfpimcclem  47643  smfsuplem1  47647  smfsupmpt  47651  smfinfmpt  47655  smflimsuplem2  47657  smflimsuplem3  47658  smflimsuplem4  47659  fsupdm  47678  finfdm  47682  tposcurf1  50233  fucocolem4  50290  veroquadgsumlem  50824