Theorem fvmptd2 7023

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105   ↦ cmpt 5230  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570

This theorem is referenced by:  fvmptopabOLD  7487  updjudhcoinlf  9969  updjudhcoinrg  9970  lcmf0val  16655  fvprmselelfz  17077  fvprmselgcd1  17078  setcval  18130  catcval  18153  estrcval  18178  hofval  18308  yonval  18317  frmdval  18876  smndex1igid  18929  smndex1n0mnd  18937  gexval  19610  rngcval  20634  ringcval  20663  frobrhm  21611  pmatcollpw3fi1lem1  22807  chfacfscmul0  22879  chfacfscmulgsum  22881  chfacfpmmul0  22883  chfacfpmmulgsum  22885  lmfval  23255  kgenval  23558  ptval  23593  utopval  24256  ustuqtoplem  24263  utopsnneiplem  24271  tusval  24289  blfvalps  24408  tmsval  24508  metuval  24577  caufval  25322  dchrval  27292  gausslemma2dlem2  27425  gausslemma2dlem3  27426  israg  28719  perpln1  28732  perpln2  28733  isperp  28734  vtxdgfval  29499  crctcsh  29853  clwlkclwwlklem2fv1  30023  clwlkclwwlklem2fv2  30024  cofmpt2  32650  pwrssmgc  32974  gsumfs2d  33040  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  rlocf1  33259  fracval  33285  qusima  33415  elrspunidl  33435  elrspunsn  33436  zringfrac  33561  r1pquslmic  33610  constrsuc  33742  madjusmdetlem2  33788  metidval  33850  pstmval  33855  carsgval  34284  bj-rdg0gALT  37053  bj-finsumval0  37267  cdleme31fv2  40375  fiabv  42522  iunrelexpmin1  43697  iunrelexpmin2  43701  rfovcnvf1od  43993  limsup10exlem  45727  dvnprodlem1  45901  prproropf1olem3  47429  prprval  47438  isuspgrim0lem  47808  clintopval  48047  1arymaptfo  48492  2arymptfv  48499  2arymaptfo  48503  ackval42  48545