Theorem fvmptd2 7007

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107   ↦ cmpt 5232  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-iota 6496  df-fun 6546  df-fv 6552

This theorem is referenced by:  fvmptopabOLD  7464  updjudhcoinlf  9927  updjudhcoinrg  9928  lcmf0val  16559  fvprmselelfz  16977  fvprmselgcd1  16978  setcval  18027  catcval  18050  estrcval  18075  hofval  18205  yonval  18214  frmdval  18732  smndex1igid  18785  smndex1n0mnd  18793  gexval  19446  pmatcollpw3fi1lem1  22288  chfacfscmul0  22360  chfacfscmulgsum  22362  chfacfpmmul0  22364  chfacfpmmulgsum  22366  lmfval  22736  kgenval  23039  ptval  23074  utopval  23737  ustuqtoplem  23744  utopsnneiplem  23752  tusval  23770  blfvalps  23889  tmsval  23989  metuval  24058  caufval  24792  dchrval  26737  gausslemma2dlem2  26870  gausslemma2dlem3  26871  israg  27979  perpln1  27992  perpln2  27993  isperp  27994  vtxdgfval  28755  crctcsh  29109  clwlkclwwlklem2fv1  29279  clwlkclwwlklem2fv2  29280  cofmpt2  31889  pwrssmgc  32201  frobrhm  32413  qusima  32550  elrspunidl  32577  elrspunsn  32578  metidval  32901  pstmval  32906  carsgval  33333  bj-rdg0gALT  36000  bj-finsumval0  36214  cdleme31fv2  39312  iunrelexpmin1  42507  iunrelexpmin2  42511  rfovcnvf1od  42803  limsup10exlem  44536  prproropf1olem3  46221  prprval  46230  clintopval  46662  rngcval  46908  ringcval  46954  1arymaptfo  47377  2arymptfv  47384  2arymaptfo  47388  ackval42  47430