Theorem fvmptd2 6976

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5188  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519

This theorem is referenced by:  fvmptopabOLD  7444  updjudhcoinlf  9885  updjudhcoinrg  9886  lcmf0val  16592  fvprmselelfz  17015  fvprmselgcd1  17016  setcval  18039  catcval  18062  estrcval  18085  hofval  18213  yonval  18222  frmdval  18778  smndex1igid  18831  smndex1n0mnd  18839  gexval  19508  rngcval  20527  ringcval  20556  frobrhm  21485  pmatcollpw3fi1lem1  22673  chfacfscmul0  22745  chfacfscmulgsum  22747  chfacfpmmul0  22749  chfacfpmmulgsum  22751  lmfval  23119  kgenval  23422  ptval  23457  utopval  24120  ustuqtoplem  24127  utopsnneiplem  24135  tusval  24153  blfvalps  24271  tmsval  24369  metuval  24437  caufval  25175  dchrval  27145  gausslemma2dlem2  27278  gausslemma2dlem3  27279  israg  28624  perpln1  28637  perpln2  28638  isperp  28639  vtxdgfval  29395  crctcsh  29754  clwlkclwwlklem2fv1  29924  clwlkclwwlklem2fv2  29925  cofmpt2  32558  pwrssmgc  32926  gsumfs2d  32995  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  rlocf1  33224  fracval  33254  qusima  33379  elrspunidl  33399  elrspunsn  33400  zringfrac  33525  r1pquslmic  33576  fldextrspunlsp  33669  constrsuc  33728  madjusmdetlem2  33818  metidval  33880  pstmval  33885  carsgval  34294  bj-rdg0gALT  37059  bj-finsumval0  37273  cdleme31fv2  40387  fiabv  42524  iunrelexpmin1  43697  iunrelexpmin2  43701  rfovcnvf1od  43993  limsup10exlem  45770  dvnprodlem1  45944  prproropf1olem3  47506  prprval  47515  isuspgrim0lem  47893  clintopval  48192  1arymaptfo  48632  2arymptfv  48639  2arymaptfo  48643  ackval42  48685