Theorem fvmptd2 6949

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5179  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  updjudhcoinlf  9844  updjudhcoinrg  9845  lcmf0val  16549  fvprmselelfz  16972  fvprmselgcd1  16973  setcval  18001  catcval  18024  estrcval  18047  hofval  18175  yonval  18184  frmdval  18776  smndex1igid  18829  smndex1n0mnd  18837  gexval  19507  rngcval  20551  ringcval  20580  frobrhm  21530  pmatcollpw3fi1lem1  22730  chfacfscmul0  22802  chfacfscmulgsum  22804  chfacfpmmul0  22806  chfacfpmmulgsum  22808  lmfval  23176  kgenval  23479  ptval  23514  utopval  24176  ustuqtoplem  24183  utopsnneiplem  24191  tusval  24209  blfvalps  24327  tmsval  24425  metuval  24493  caufval  25231  dchrval  27201  gausslemma2dlem2  27334  gausslemma2dlem3  27335  israg  28769  perpln1  28782  perpln2  28783  isperp  28784  vtxdgfval  29541  crctcsh  29897  clwlkclwwlklem2fv1  30070  clwlkclwwlklem2fv2  30071  cofmpt2  32712  pwrssmgc  33082  gsumfs2d  33144  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  rlocf1  33355  fracval  33386  qusima  33489  elrspunidl  33509  elrspunsn  33510  zringfrac  33635  r1pquslmic  33692  mplvrpmmhm  33711  mplvrpmrhm  33712  fldextrspunlsp  33831  constrsuc  33895  madjusmdetlem2  33985  metidval  34047  pstmval  34052  carsgval  34460  bj-rdg0gALT  37272  bj-finsumval0  37486  cdleme31fv2  40649  fiabv  42787  iunrelexpmin1  43945  iunrelexpmin2  43949  rfovcnvf1od  44241  limsup10exlem  46012  dvnprodlem1  46186  prproropf1olem3  47747  prprval  47756  isuspgrim0lem  48135  clintopval  48446  1arymaptfo  48885  2arymptfv  48892  2arymaptfo  48896  ackval42  48938