Theorem fvmptd2 6994

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ↦ cmpt 5201  ‘cfv 6531

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6484  df-fun 6533  df-fv 6539

This theorem is referenced by:  fvmptopabOLD  7462  updjudhcoinlf  9946  updjudhcoinrg  9947  lcmf0val  16641  fvprmselelfz  17064  fvprmselgcd1  17065  setcval  18090  catcval  18113  estrcval  18136  hofval  18264  yonval  18273  frmdval  18829  smndex1igid  18882  smndex1n0mnd  18890  gexval  19559  rngcval  20578  ringcval  20607  frobrhm  21536  pmatcollpw3fi1lem1  22724  chfacfscmul0  22796  chfacfscmulgsum  22798  chfacfpmmul0  22800  chfacfpmmulgsum  22802  lmfval  23170  kgenval  23473  ptval  23508  utopval  24171  ustuqtoplem  24178  utopsnneiplem  24186  tusval  24204  blfvalps  24322  tmsval  24420  metuval  24488  caufval  25227  dchrval  27197  gausslemma2dlem2  27330  gausslemma2dlem3  27331  israg  28676  perpln1  28689  perpln2  28690  isperp  28691  vtxdgfval  29447  crctcsh  29806  clwlkclwwlklem2fv1  29976  clwlkclwwlklem2fv2  29977  cofmpt2  32612  pwrssmgc  32980  gsumfs2d  33049  elrgspnlem2  33238  elrgspnlem3  33239  elrgspnlem4  33240  rlocf1  33268  fracval  33298  qusima  33423  elrspunidl  33443  elrspunsn  33444  zringfrac  33569  r1pquslmic  33620  fldextrspunlsp  33715  constrsuc  33772  madjusmdetlem2  33859  metidval  33921  pstmval  33926  carsgval  34335  bj-rdg0gALT  37089  bj-finsumval0  37303  cdleme31fv2  40412  fiabv  42559  iunrelexpmin1  43732  iunrelexpmin2  43736  rfovcnvf1od  44028  limsup10exlem  45801  dvnprodlem1  45975  prproropf1olem3  47519  prprval  47528  isuspgrim0lem  47906  clintopval  48179  1arymaptfo  48623  2arymptfv  48630  2arymaptfo  48634  ackval42  48676