Theorem fvmptd2 6883

Description: Deduction version of fvmpt 6875 (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 6882	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106   ↦ cmpt 5157  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441

This theorem is referenced by:  fvmptopabOLD  7330  updjudhcoinlf  9690  updjudhcoinrg  9691  lcmf0val  16327  fvprmselelfz  16745  fvprmselgcd1  16746  setcval  17792  catcval  17815  estrcval  17840  hofval  17970  yonval  17979  frmdval  18490  smndex1igid  18543  smndex1n0mnd  18551  gexval  19183  pmatcollpw3fi1lem1  21935  chfacfscmul0  22007  chfacfscmulgsum  22009  chfacfpmmul0  22011  chfacfpmmulgsum  22013  lmfval  22383  kgenval  22686  ptval  22721  utopval  23384  ustuqtoplem  23391  utopsnneiplem  23399  tusval  23417  blfvalps  23536  tmsval  23636  metuval  23705  caufval  24439  dchrval  26382  gausslemma2dlem2  26515  gausslemma2dlem3  26516  israg  27058  perpln1  27071  perpln2  27072  isperp  27073  vtxdgfval  27834  crctcsh  28189  clwlkclwwlklem2fv1  28359  clwlkclwwlklem2fv2  28360  cofmpt2  30969  pwrssmgc  31278  frobrhm  31485  qusima  31594  elrspunidl  31606  carsgval  32270  bj-rdg0gALT  35242  bj-finsumval0  35456  cdleme31fv2  38407  iunrelexpmin1  41316  iunrelexpmin2  41320  rfovcnvf1od  41612  limsup10exlem  43313  prproropf1olem3  44957  prprval  44966  clintopval  45398  rngcval  45520  ringcval  45566  1arymaptfo  45989  2arymptfv  45996  2arymaptfo  46000  ackval42  46042