Theorem fvmptd2 6999

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5190  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is used by:  updjudhcoinlf  9941  updjudhcoinrg  9942  lcmf0val  16718  fvprmselelfz  17142  fvprmselgcd1  17143  setcval  18172  catcval  18195  estrcval  18218  hofval  18346  yonval  18355  frmdval  18966  smndex1igid  19021  smndex1igidOLD  19022  smndex1n0mnd  19030  gexval  19711  rngcval  20786  ringcval  20815  frobrhm  21794  pmatcollpw3fi1lem1  23017  chfacfscmul0  23089  chfacfscmulgsum  23091  chfacfpmmul0  23093  chfacfpmmulgsum  23095  lmfval  23463  kgenval  23767  ptval  23802  utopval  24464  ustuqtoplem  24471  utopsnneiplem  24479  tusval  24497  blfvalps  24615  tmsval  24713  metuval  24781  caufval  25509  dchrval  27478  gausslemma2dlem2  27611  gausslemma2dlem3  27612  israg  29059  perpln1  29072  perpln2  29073  isperp  29074  vtxdgfval  29935  crctcsh  30300  clwlkclwwlklem2fv1  30473  clwlkclwwlklem2fv2  30474  cofmpt2  33115  pwrssmgc  33448  gsumfs2d  33509  elrgspnlem2  33691  elrgspnlem3  33692  elrgspnlem4  33693  rlocf1  33722  fracval  33753  qusima  33845  elrspunidl  33864  elrspunsn  33865  zringfrac  33972  r1pquslmic  34028  0mplrim  34032  selvply1rhmlemb  34037  selvply1rhmlem2  34039  selvply1rhmlem4  34041  mplvrpmmhm  34064  mplvrpmrhm  34065  psrmonprod  34070  esplyfvaln  34092  fldextrspunlsp  34192  constrsuc  34256  madjusmdetlem2  34346  metidval  34408  pstmval  34413  carsgval  34822  dfttc3gw  37150  bj-rdg0gALT  37823  bj-finsumval0  38045  cdleme31fv2  41274  fiabv  43426  iunrelexpmin1  44556  iunrelexpmin2  44560  rfovcnvf1od  44852  limsup10exlem  46608  dvnprodlem1  46782  prproropf1olem3  48413  prprval  48422  isuspgrim0lem  48817  clintopval  49127  1arymaptfo  49581  2arymptfv  49588  2arymaptfo  49592  ackval42  49634