Theorem fvmptd2 6943

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

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

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 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  updjudhcoinlf  9832  updjudhcoinrg  9833  lcmf0val  16535  fvprmselelfz  16958  fvprmselgcd1  16959  setcval  17986  catcval  18009  estrcval  18032  hofval  18160  yonval  18169  frmdval  18761  smndex1igid  18814  smndex1n0mnd  18822  gexval  19492  rngcval  20535  ringcval  20564  frobrhm  21514  pmatcollpw3fi1lem1  22702  chfacfscmul0  22774  chfacfscmulgsum  22776  chfacfpmmul0  22778  chfacfpmmulgsum  22780  lmfval  23148  kgenval  23451  ptval  23486  utopval  24148  ustuqtoplem  24155  utopsnneiplem  24163  tusval  24181  blfvalps  24299  tmsval  24397  metuval  24465  caufval  25203  dchrval  27173  gausslemma2dlem2  27306  gausslemma2dlem3  27307  israg  28676  perpln1  28689  perpln2  28690  isperp  28691  vtxdgfval  29448  crctcsh  29804  clwlkclwwlklem2fv1  29977  clwlkclwwlklem2fv2  29978  cofmpt2  32618  pwrssmgc  32988  gsumfs2d  33042  elrgspnlem2  33217  elrgspnlem3  33218  elrgspnlem4  33219  rlocf1  33247  fracval  33277  qusima  33380  elrspunidl  33400  elrspunsn  33401  zringfrac  33526  r1pquslmic  33578  mplvrpmmhm  33594  mplvrpmrhm  33595  fldextrspunlsp  33708  constrsuc  33772  madjusmdetlem2  33862  metidval  33924  pstmval  33929  carsgval  34337  bj-rdg0gALT  37136  bj-finsumval0  37350  cdleme31fv2  40513  fiabv  42655  iunrelexpmin1  43826  iunrelexpmin2  43830  rfovcnvf1od  44122  limsup10exlem  45895  dvnprodlem1  46069  prproropf1olem3  47630  prprval  47639  isuspgrim0lem  48018  clintopval  48329  1arymaptfo  48769  2arymptfv  48776  2arymaptfo  48780  ackval42  48822