Theorem fvmptd2 6942

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

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

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 5238  ax-nul 5248  ax-pr 5374

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 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  updjudhcoinlf  9847  updjudhcoinrg  9848  lcmf0val  16551  fvprmselelfz  16974  fvprmselgcd1  16975  setcval  18002  catcval  18025  estrcval  18048  hofval  18176  yonval  18185  frmdval  18743  smndex1igid  18796  smndex1n0mnd  18804  gexval  19475  rngcval  20521  ringcval  20550  frobrhm  21500  pmatcollpw3fi1lem1  22689  chfacfscmul0  22761  chfacfscmulgsum  22763  chfacfpmmul0  22765  chfacfpmmulgsum  22767  lmfval  23135  kgenval  23438  ptval  23473  utopval  24136  ustuqtoplem  24143  utopsnneiplem  24151  tusval  24169  blfvalps  24287  tmsval  24385  metuval  24453  caufval  25191  dchrval  27161  gausslemma2dlem2  27294  gausslemma2dlem3  27295  israg  28660  perpln1  28673  perpln2  28674  isperp  28675  vtxdgfval  29431  crctcsh  29787  clwlkclwwlklem2fv1  29957  clwlkclwwlklem2fv2  29958  cofmpt2  32591  pwrssmgc  32955  gsumfs2d  33021  elrgspnlem2  33196  elrgspnlem3  33197  elrgspnlem4  33198  rlocf1  33226  fracval  33256  qusima  33358  elrspunidl  33378  elrspunsn  33379  zringfrac  33504  r1pquslmic  33555  fldextrspunlsp  33648  constrsuc  33707  madjusmdetlem2  33797  metidval  33859  pstmval  33864  carsgval  34273  bj-rdg0gALT  37047  bj-finsumval0  37261  cdleme31fv2  40375  fiabv  42512  iunrelexpmin1  43684  iunrelexpmin2  43688  rfovcnvf1od  43980  limsup10exlem  45757  dvnprodlem1  45931  prproropf1olem3  47493  prprval  47502  isuspgrim0lem  47881  clintopval  48192  1arymaptfo  48632  2arymptfv  48639  2arymaptfo  48643  ackval42  48685