Theorem fvmptd2 6958

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5181  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508

This theorem is referenced by:  updjudhcoinlf  9856  updjudhcoinrg  9857  lcmf0val  16561  fvprmselelfz  16984  fvprmselgcd1  16985  setcval  18013  catcval  18036  estrcval  18059  hofval  18187  yonval  18196  frmdval  18788  smndex1igid  18841  smndex1n0mnd  18849  gexval  19519  rngcval  20563  ringcval  20592  frobrhm  21542  pmatcollpw3fi1lem1  22742  chfacfscmul0  22814  chfacfscmulgsum  22816  chfacfpmmul0  22818  chfacfpmmulgsum  22820  lmfval  23188  kgenval  23491  ptval  23526  utopval  24188  ustuqtoplem  24195  utopsnneiplem  24203  tusval  24221  blfvalps  24339  tmsval  24437  metuval  24505  caufval  25243  dchrval  27213  gausslemma2dlem2  27346  gausslemma2dlem3  27347  israg  28781  perpln1  28794  perpln2  28795  isperp  28796  vtxdgfval  29553  crctcsh  29909  clwlkclwwlklem2fv1  30082  clwlkclwwlklem2fv2  30083  cofmpt2  32723  pwrssmgc  33092  gsumfs2d  33154  elrgspnlem2  33336  elrgspnlem3  33337  elrgspnlem4  33338  rlocf1  33366  fracval  33397  qusima  33500  elrspunidl  33520  elrspunsn  33521  zringfrac  33646  r1pquslmic  33703  mplvrpmmhm  33722  mplvrpmrhm  33723  psrmonprod  33728  esplyfvaln  33750  fldextrspunlsp  33851  constrsuc  33915  madjusmdetlem2  34005  metidval  34067  pstmval  34072  carsgval  34480  bj-rdg0gALT  37313  bj-finsumval0  37534  cdleme31fv2  40763  fiabv  42900  iunrelexpmin1  44058  iunrelexpmin2  44062  rfovcnvf1od  44354  limsup10exlem  46124  dvnprodlem1  46298  prproropf1olem3  47859  prprval  47868  isuspgrim0lem  48247  clintopval  48558  1arymaptfo  48997  2arymptfv  49004  2arymaptfo  49008  ackval42  49050