Theorem fvmptd2 7024

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ↦ cmpt 5225  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569

This theorem is referenced by:  fvmptopabOLD  7488  updjudhcoinlf  9972  updjudhcoinrg  9973  lcmf0val  16659  fvprmselelfz  17082  fvprmselgcd1  17083  setcval  18122  catcval  18145  estrcval  18168  hofval  18297  yonval  18306  frmdval  18864  smndex1igid  18917  smndex1n0mnd  18925  gexval  19596  rngcval  20618  ringcval  20647  frobrhm  21594  pmatcollpw3fi1lem1  22792  chfacfscmul0  22864  chfacfscmulgsum  22866  chfacfpmmul0  22868  chfacfpmmulgsum  22870  lmfval  23240  kgenval  23543  ptval  23578  utopval  24241  ustuqtoplem  24248  utopsnneiplem  24256  tusval  24274  blfvalps  24393  tmsval  24493  metuval  24562  caufval  25309  dchrval  27278  gausslemma2dlem2  27411  gausslemma2dlem3  27412  israg  28705  perpln1  28718  perpln2  28719  isperp  28720  vtxdgfval  29485  crctcsh  29844  clwlkclwwlklem2fv1  30014  clwlkclwwlklem2fv2  30015  cofmpt2  32644  pwrssmgc  32990  gsumfs2d  33058  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  rlocf1  33277  fracval  33306  qusima  33436  elrspunidl  33456  elrspunsn  33457  zringfrac  33582  r1pquslmic  33631  fldextrspunlsp  33724  constrsuc  33779  madjusmdetlem2  33827  metidval  33889  pstmval  33894  carsgval  34305  bj-rdg0gALT  37072  bj-finsumval0  37286  cdleme31fv2  40395  fiabv  42546  iunrelexpmin1  43721  iunrelexpmin2  43725  rfovcnvf1od  44017  limsup10exlem  45787  dvnprodlem1  45961  prproropf1olem3  47492  prprval  47501  isuspgrim0lem  47871  clintopval  48120  1arymaptfo  48564  2arymptfv  48571  2arymaptfo  48575  ackval42  48617