Theorem fvmptd2 6938

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5173  ‘cfv 6482

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6438  df-fun 6484  df-fv 6490

This theorem is referenced by:  updjudhcoinlf  9828  updjudhcoinrg  9829  lcmf0val  16533  fvprmselelfz  16956  fvprmselgcd1  16957  setcval  17984  catcval  18007  estrcval  18030  hofval  18158  yonval  18167  frmdval  18725  smndex1igid  18778  smndex1n0mnd  18786  gexval  19457  rngcval  20503  ringcval  20532  frobrhm  21482  pmatcollpw3fi1lem1  22671  chfacfscmul0  22743  chfacfscmulgsum  22745  chfacfpmmul0  22747  chfacfpmmulgsum  22749  lmfval  23117  kgenval  23420  ptval  23455  utopval  24118  ustuqtoplem  24125  utopsnneiplem  24133  tusval  24151  blfvalps  24269  tmsval  24367  metuval  24435  caufval  25173  dchrval  27143  gausslemma2dlem2  27276  gausslemma2dlem3  27277  israg  28642  perpln1  28655  perpln2  28656  isperp  28657  vtxdgfval  29413  crctcsh  29769  clwlkclwwlklem2fv1  29939  clwlkclwwlklem2fv2  29940  cofmpt2  32577  pwrssmgc  32942  gsumfs2d  33008  elrgspnlem2  33183  elrgspnlem3  33184  elrgspnlem4  33185  rlocf1  33213  fracval  33243  qusima  33345  elrspunidl  33365  elrspunsn  33366  zringfrac  33491  r1pquslmic  33543  fldextrspunlsp  33641  constrsuc  33705  madjusmdetlem2  33795  metidval  33857  pstmval  33862  carsgval  34271  bj-rdg0gALT  37045  bj-finsumval0  37259  cdleme31fv2  40372  fiabv  42509  iunrelexpmin1  43681  iunrelexpmin2  43685  rfovcnvf1od  43977  limsup10exlem  45753  dvnprodlem1  45927  prproropf1olem3  47489  prprval  47498  isuspgrim0lem  47877  clintopval  48188  1arymaptfo  48628  2arymptfv  48635  2arymaptfo  48639  ackval42  48681