Theorem fvmptd2 7002

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ↦ cmpt 5185  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6540  df-fv 6546

This theorem is used by:  updjudhcoinlf  10016  updjudhcoinrg  10017  lcmf0val  16802  fvprmselelfz  17227  fvprmselgcd1  17228  setcval  18257  catcval  18280  estrcval  18303  hofval  18431  yonval  18440  frmdval  19052  smndex1igid  19107  smndex1igidOLD  19108  smndex1n0mnd  19116  gexval  19797  rngcval  20875  ringcval  20904  frobrhm  21886  pmatcollpw3fi1lem1  23109  chfacfscmul0  23181  chfacfscmulgsum  23183  chfacfpmmul0  23185  chfacfpmmulgsum  23187  lmfval  23555  kgenval  23859  ptval  23894  utopval  24556  ustuqtoplem  24563  utopsnneiplem  24571  tusval  24589  blfvalps  24707  tmsval  24805  metuval  24873  caufval  25601  dchrval  27566  gausslemma2dlem2  27699  gausslemma2dlem3  27700  israg  29177  perpln1  29190  perpln2  29191  isperp  29192  vtxdgfval  30053  crctcsh  30418  clwlkclwwlklem2fv1  30591  clwlkclwwlklem2fv2  30592  cofmpt2  33275  pwrssmgc  33607  gsumfs2d  33668  elrgspnlem2  33850  elrgspnlem3  33851  elrgspnlem4  33852  rlocf1  33881  fracval  33912  qusima  34005  elrspunidl  34024  elrspunsn  34025  zringfrac  34132  r1pquslmic  34188  0mplrim  34192  selvply1rhmlemb  34197  selvply1rhmlem2  34199  selvply1rhmlem4  34201  mplvrpmmhm  34224  mplvrpmrhm  34225  psrmonprod  34230  esplyfvaln  34252  fldextrspunlsp  34352  constrsuc  34416  madjusmdetlem2  34506  metidval  34568  pstmval  34573  carsgval  34981  dfttc3gw  37403  bj-rdg0gALT  38078  bj-finsumval0  38299  cdleme31fv2  41543  fiabv  43693  iunrelexpmin1  44801  iunrelexpmin2  44805  rfovcnvf1od  45097  limsup10exlem  46875  dvnprodlem1  47049  prproropf1olem3  48680  prprval  48689  isuspgrim0lem  49084  clintopval  49394  1arymaptfo  49848  2arymptfv  49855  2arymaptfo  49859  ackval42  49901  parmapfunc2  50867