Theorem fvmptd2 6980

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ↦ cmpt 5180  ‘cfv 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-iota 6473  df-fun 6519  df-fv 6525

This theorem is referenced by:  updjudhcoinlf  9887  updjudhcoinrg  9888  lcmf0val  16639  fvprmselelfz  17063  fvprmselgcd1  17064  setcval  18093  catcval  18116  estrcval  18139  hofval  18267  yonval  18276  frmdval  18868  smndex1igid  18923  smndex1igidOLD  18924  smndex1n0mnd  18932  gexval  19601  rngcval  20647  ringcval  20676  frobrhm  21607  pmatcollpw3fi1lem1  22826  chfacfscmul0  22898  chfacfscmulgsum  22900  chfacfpmmul0  22902  chfacfpmmulgsum  22904  lmfval  23272  kgenval  23575  ptval  23610  utopval  24272  ustuqtoplem  24279  utopsnneiplem  24287  tusval  24305  blfvalps  24423  tmsval  24521  metuval  24589  caufval  25317  dchrval  27275  gausslemma2dlem2  27408  gausslemma2dlem3  27409  israg  28843  perpln1  28856  perpln2  28857  isperp  28858  vtxdgfval  29614  crctcsh  29970  clwlkclwwlklem2fv1  30143  clwlkclwwlklem2fv2  30144  cofmpt2  32786  pwrssmgc  33139  gsumfs2d  33202  elrgspnlem2  33385  elrgspnlem3  33386  elrgspnlem4  33387  rlocf1  33416  fracval  33452  qusima  33555  elrspunidl  33575  elrspunsn  33576  zringfrac  33711  r1pquslmic  33768  0mplrim  33772  selvply1rhmlemb  33777  selvply1rhmlem2  33779  selvply1rhmlem4  33781  mplvrpmmhm  33804  mplvrpmrhm  33805  psrmonprod  33810  esplyfvaln  33832  fldextrspunlsp  33932  constrsuc  33996  madjusmdetlem2  34086  metidval  34148  pstmval  34153  carsgval  34561  dfttc3gw  36847  bj-rdg0gALT  37520  bj-finsumval0  37741  cdleme31fv2  40981  fiabv  43118  iunrelexpmin1  44248  iunrelexpmin2  44252  rfovcnvf1od  44544  limsup10exlem  46310  dvnprodlem1  46484  prproropf1olem3  48075  prprval  48084  isuspgrim0lem  48479  clintopval  48790  1arymaptfo  49229  2arymptfv  49236  2arymaptfo  49240  ackval42  49282