Theorem fvmptd2 6951

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ↦ cmpt 5160  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  updjudhcoinlf  9854  updjudhcoinrg  9855  lcmf0val  16589  fvprmselelfz  17013  fvprmselgcd1  17014  setcval  18042  catcval  18065  estrcval  18088  hofval  18216  yonval  18225  frmdval  18817  smndex1igid  18872  smndex1igidOLD  18873  smndex1n0mnd  18881  gexval  19551  rngcval  20597  ringcval  20626  frobrhm  21557  pmatcollpw3fi1lem1  22776  chfacfscmul0  22848  chfacfscmulgsum  22850  chfacfpmmul0  22852  chfacfpmmulgsum  22854  lmfval  23222  kgenval  23525  ptval  23560  utopval  24222  ustuqtoplem  24229  utopsnneiplem  24237  tusval  24255  blfvalps  24373  tmsval  24471  metuval  24539  caufval  25267  dchrval  27222  gausslemma2dlem2  27355  gausslemma2dlem3  27356  israg  28790  perpln1  28803  perpln2  28804  isperp  28805  vtxdgfval  29561  crctcsh  29917  clwlkclwwlklem2fv1  30090  clwlkclwwlklem2fv2  30091  cofmpt2  32733  pwrssmgc  33086  gsumfs2d  33149  elrgspnlem2  33331  elrgspnlem3  33332  elrgspnlem4  33333  rlocf1  33361  fracval  33395  qusima  33498  elrspunidl  33518  elrspunsn  33519  zringfrac  33644  r1pquslmic  33701  0mplrim  33705  selvply1rhmlemb  33710  selvply1rhmlem2  33712  selvply1rhmlem4  33714  mplvrpmmhm  33737  mplvrpmrhm  33738  psrmonprod  33743  esplyfvaln  33765  fldextrspunlsp  33865  constrsuc  33929  madjusmdetlem2  34019  metidval  34081  pstmval  34086  carsgval  34494  dfttc3gw  36758  bj-rdg0gALT  37431  bj-finsumval0  37652  cdleme31fv2  40892  fiabv  43029  iunrelexpmin1  44159  iunrelexpmin2  44163  rfovcnvf1od  44455  limsup10exlem  46222  dvnprodlem1  46396  prproropf1olem3  47987  prprval  47996  isuspgrim0lem  48391  clintopval  48702  1arymaptfo  49141  2arymptfv  49148  2arymaptfo  49152  ackval42  49194