Theorem fvmptd2 7025

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 7024	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ↦ cmpt 5189  ‘cfv 6558

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6512  df-fun 6560  df-fv 6566

This theorem is used by:  updjudhcoinlf  10040  updjudhcoinrg  10041  lcmf0val  16826  fvprmselelfz  17251  fvprmselgcd1  17252  setcval  18281  catcval  18304  estrcval  18327  hofval  18455  yonval  18464  frmdval  19076  smndex1igid  19131  smndex1igidOLD  19132  smndex1n0mnd  19140  gexval  19822  rngcval  20900  ringcval  20929  frobrhm  21911  pmatcollpw3fi1lem1  23134  chfacfscmul0  23206  chfacfscmulgsum  23208  chfacfpmmul0  23210  chfacfpmmulgsum  23212  lmfval  23580  kgenval  23884  ptval  23919  utopval  24581  ustuqtoplem  24588  utopsnneiplem  24596  tusval  24614  blfvalps  24732  tmsval  24830  metuval  24898  caufval  25626  dchrval  27591  gausslemma2dlem2  27724  gausslemma2dlem3  27725  israg  29202  perpln1  29215  perpln2  29216  isperp  29217  vtxdgfval  30078  crctcsh  30443  clwlkclwwlklem2fv1  30616  clwlkclwwlklem2fv2  30617  cofmpt2  33300  pwrssmgc  33631  gsumfs2d  33692  elrgspnlem2  33874  elrgspnlem3  33875  elrgspnlem4  33876  rlocf1  33905  fracval  33936  qusima  34029  elrspunidl  34048  elrspunsn  34049  zringfrac  34156  r1pquslmic  34212  0mplrim  34216  selvply1rhmlemb  34221  selvply1rhmlem2  34223  selvply1rhmlem4  34225  mplvrpmmhm  34248  mplvrpmrhm  34249  psrmonprod  34254  esplyfvaln  34276  fldextrspunlsp  34376  constrsuc  34440  madjusmdetlem2  34530  metidval  34592  pstmval  34597  carsgval  35005  fnlfvk30  36027  fnlfvk3n0  36028  dfttc3gw  37489  bj-rdg0gALT  38177  bj-finsumval0  38398  cdleme31fv2  41642  fiabv  43793  iunrelexpmin1  44900  iunrelexpmin2  44904  rfovcnvf1od  45196  limsup10exlem  46987  dvnprodlem1  47161  prproropf1olem3  48792  prprval  48801  isuspgrim0lem  49196  clintopval  49506  1arymaptfo  49960  2arymptfv  49967  2arymaptfo  49971  ackval42  50013  parmapfunc2  50979