Theorem fvmptd2 7000

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ↦ cmpt 5193  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546

This theorem is referenced by:  updjudhcoinlf  9919  updjudhcoinrg  9920  lcmf0val  16681  fvprmselelfz  17105  fvprmselgcd1  17106  setcval  18135  catcval  18158  estrcval  18181  hofval  18309  yonval  18318  frmdval  18911  smndex1igid  18966  smndex1igidOLD  18967  smndex1n0mnd  18975  gexval  19649  rngcval  20704  ringcval  20733  frobrhm  21706  pmatcollpw3fi1lem1  22924  chfacfscmul0  22996  chfacfscmulgsum  22998  chfacfpmmul0  23000  chfacfpmmulgsum  23002  lmfval  23370  kgenval  23673  ptval  23708  utopval  24370  ustuqtoplem  24377  utopsnneiplem  24385  tusval  24403  blfvalps  24521  tmsval  24619  metuval  24687  caufval  25415  dchrval  27376  gausslemma2dlem2  27509  gausslemma2dlem3  27510  israg  28955  perpln1  28968  perpln2  28969  isperp  28970  vtxdgfval  29795  crctcsh  30151  clwlkclwwlklem2fv1  30324  clwlkclwwlklem2fv2  30325  cofmpt2  32957  pwrssmgc  33298  gsumfs2d  33359  elrgspnlem2  33541  elrgspnlem3  33542  elrgspnlem4  33543  rlocf1  33572  fracval  33603  qusima  33695  elrspunidl  33714  elrspunsn  33715  zringfrac  33822  r1pquslmic  33878  0mplrim  33882  selvply1rhmlemb  33887  selvply1rhmlem2  33889  selvply1rhmlem4  33891  mplvrpmmhm  33914  mplvrpmrhm  33915  psrmonprod  33920  esplyfvaln  33942  fldextrspunlsp  34042  constrsuc  34106  madjusmdetlem2  34196  metidval  34258  pstmval  34263  carsgval  34671  dfttc3gw  37012  bj-rdg0gALT  37685  bj-finsumval0  37907  cdleme31fv2  41145  fiabv  43284  iunrelexpmin1  44414  iunrelexpmin2  44418  rfovcnvf1od  44710  limsup10exlem  46466  dvnprodlem1  46640  prproropf1olem3  48231  prprval  48240  isuspgrim0lem  48635  clintopval  48946  1arymaptfo  49400  2arymptfv  49407  2arymaptfo  49411  ackval42  49453