Theorem fvmptd2 6865

Description: Deduction version of fvmpt 6857 (where the definition of the mapping does not depend on the common antecedent 𝜑). (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

Ref	Expression
fvmptd2.1	⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
fvmptd2.2	⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
fvmptd2.3	⊢ (𝜑 → 𝐴 ∈ 𝐷)
fvmptd2.4	⊢ (𝜑 → 𝐶 ∈ 𝑉)

Assertion

Ref	Expression
fvmptd2	⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷   𝜑,𝑥

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fvmptd2

Step	Hyp	Ref	Expression
1		fvmptd2.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵))
3		fvmptd2.2	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
4		fvmptd2.3	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
5		fvmptd2.4	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
6	2, 3, 4, 5	fvmptd 6864	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108   ↦ cmpt 5153  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426

This theorem is referenced by:  fvmptopab  7308  updjudhcoinlf  9621  updjudhcoinrg  9622  lcmf0val  16255  fvprmselelfz  16673  fvprmselgcd1  16674  setcval  17708  catcval  17731  estrcval  17756  hofval  17886  yonval  17895  frmdval  18405  smndex1igid  18458  smndex1n0mnd  18466  gexval  19098  pmatcollpw3fi1lem1  21843  chfacfscmul0  21915  chfacfscmulgsum  21917  chfacfpmmul0  21919  chfacfpmmulgsum  21921  lmfval  22291  kgenval  22594  ptval  22629  utopval  23292  ustuqtoplem  23299  utopsnneiplem  23307  tusval  23325  blfvalps  23444  tmsval  23542  metuval  23611  caufval  24344  dchrval  26287  gausslemma2dlem2  26420  gausslemma2dlem3  26421  israg  26962  perpln1  26975  perpln2  26976  isperp  26977  vtxdgfval  27737  crctcsh  28090  clwlkclwwlklem2fv1  28260  clwlkclwwlklem2fv2  28261  cofmpt2  30870  pwrssmgc  31180  frobrhm  31387  qusima  31496  elrspunidl  31508  carsgval  32170  bj-rdg0gALT  35169  bj-finsumval0  35383  cdleme31fv2  38334  iunrelexpmin1  41205  iunrelexpmin2  41209  rfovcnvf1od  41501  limsup10exlem  43203  prproropf1olem3  44845  prprval  44854  clintopval  45286  rngcval  45408  ringcval  45454  1arymaptfo  45877  2arymptfv  45884  2arymaptfo  45888  ackval42  45930