Theorem fvmptd2 6826

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2110   ↦ cmpt 5135  ‘cfv 6380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-iota 6338  df-fun 6382  df-fv 6388

This theorem is referenced by:  fvmptopab  7266  updjudhcoinlf  9548  updjudhcoinrg  9549  lcmf0val  16179  fvprmselelfz  16597  fvprmselgcd1  16598  setcval  17583  catcval  17606  estrcval  17631  hofval  17760  yonval  17769  frmdval  18278  smndex1igid  18331  smndex1n0mnd  18339  gexval  18967  pmatcollpw3fi1lem1  21683  chfacfscmul0  21755  chfacfscmulgsum  21757  chfacfpmmul0  21759  chfacfpmmulgsum  21761  lmfval  22129  kgenval  22432  ptval  22467  utopval  23130  ustuqtoplem  23137  utopsnneiplem  23145  tusval  23163  blfvalps  23281  tmsval  23379  metuval  23447  caufval  24172  dchrval  26115  gausslemma2dlem2  26248  gausslemma2dlem3  26249  israg  26788  perpln1  26801  perpln2  26802  isperp  26803  vtxdgfval  27555  crctcsh  27908  clwlkclwwlklem2fv1  28078  clwlkclwwlklem2fv2  28079  cofmpt2  30688  pwrssmgc  30997  frobrhm  31204  qusima  31308  elrspunidl  31320  carsgval  31982  bj-finsumval0  35191  cdleme31fv2  38144  iunrelexpmin1  40993  iunrelexpmin2  40997  rfovcnvf1od  41289  limsup10exlem  42988  prproropf1olem3  44630  prprval  44639  clintopval  45071  rngcval  45193  ringcval  45239  1arymaptfo  45662  2arymptfv  45669  2arymaptfo  45673  ackval42  45715