Theorem fvmptd2 6988

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145   ↦ cmpt 5186  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-iota 6481  df-fun 6527  df-fv 6533

This theorem is referenced by:  updjudhcoinlf  9906  updjudhcoinrg  9907  lcmf0val  16670  fvprmselelfz  17094  fvprmselgcd1  17095  setcval  18124  catcval  18147  estrcval  18170  hofval  18298  yonval  18307  frmdval  18900  smndex1igid  18955  smndex1igidOLD  18956  smndex1n0mnd  18964  gexval  19639  rngcval  20694  ringcval  20723  frobrhm  21685  pmatcollpw3fi1lem1  22904  chfacfscmul0  22976  chfacfscmulgsum  22978  chfacfpmmul0  22980  chfacfpmmulgsum  22982  lmfval  23350  kgenval  23653  ptval  23688  utopval  24350  ustuqtoplem  24357  utopsnneiplem  24365  tusval  24383  blfvalps  24501  tmsval  24599  metuval  24667  caufval  25395  dchrval  27356  gausslemma2dlem2  27489  gausslemma2dlem3  27490  israg  28928  perpln1  28941  perpln2  28942  isperp  28943  vtxdgfval  29726  crctcsh  30082  clwlkclwwlklem2fv1  30255  clwlkclwwlklem2fv2  30256  cofmpt2  32891  pwrssmgc  33233  gsumfs2d  33294  elrgspnlem2  33476  elrgspnlem3  33477  elrgspnlem4  33478  rlocf1  33507  fracval  33540  qusima  33633  elrspunidl  33652  elrspunsn  33653  zringfrac  33761  r1pquslmic  33817  0mplrim  33821  selvply1rhmlemb  33826  selvply1rhmlem2  33828  selvply1rhmlem4  33830  mplvrpmmhm  33853  mplvrpmrhm  33854  psrmonprod  33859  esplyfvaln  33881  fldextrspunlsp  33981  constrsuc  34045  madjusmdetlem2  34135  metidval  34197  pstmval  34202  carsgval  34610  dfttc3gw  36896  bj-rdg0gALT  37568  bj-finsumval0  37789  cdleme31fv2  41029  fiabv  43166  iunrelexpmin1  44296  iunrelexpmin2  44300  rfovcnvf1od  44592  limsup10exlem  46344  dvnprodlem1  46518  prproropf1olem3  48109  prprval  48118  isuspgrim0lem  48513  clintopval  48824  1arymaptfo  49274  2arymptfv  49281  2arymaptfo  49285  ackval42  49327