Theorem fvmptd2 6956

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5166  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506

This theorem is referenced by:  updjudhcoinlf  9856  updjudhcoinrg  9857  lcmf0val  16591  fvprmselelfz  17015  fvprmselgcd1  17016  setcval  18044  catcval  18067  estrcval  18090  hofval  18218  yonval  18227  frmdval  18819  smndex1igid  18874  smndex1igidOLD  18875  smndex1n0mnd  18883  gexval  19553  rngcval  20595  ringcval  20624  frobrhm  21555  pmatcollpw3fi1lem1  22751  chfacfscmul0  22823  chfacfscmulgsum  22825  chfacfpmmul0  22827  chfacfpmmulgsum  22829  lmfval  23197  kgenval  23500  ptval  23535  utopval  24197  ustuqtoplem  24204  utopsnneiplem  24212  tusval  24230  blfvalps  24348  tmsval  24446  metuval  24514  caufval  25242  dchrval  27197  gausslemma2dlem2  27330  gausslemma2dlem3  27331  israg  28765  perpln1  28778  perpln2  28779  isperp  28780  vtxdgfval  29536  crctcsh  29892  clwlkclwwlklem2fv1  30065  clwlkclwwlklem2fv2  30066  cofmpt2  32707  pwrssmgc  33060  gsumfs2d  33122  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  rlocf1  33334  fracval  33365  qusima  33468  elrspunidl  33488  elrspunsn  33489  zringfrac  33614  r1pquslmic  33671  mplvrpmmhm  33690  mplvrpmrhm  33691  psrmonprod  33696  esplyfvaln  33718  fldextrspunlsp  33818  constrsuc  33882  madjusmdetlem2  33972  metidval  34034  pstmval  34039  carsgval  34447  dfttc3gw  36705  bj-rdg0gALT  37378  bj-finsumval0  37599  cdleme31fv2  40839  fiabv  42981  iunrelexpmin1  44135  iunrelexpmin2  44139  rfovcnvf1od  44431  limsup10exlem  46200  dvnprodlem1  46374  prproropf1olem3  47965  prprval  47974  isuspgrim0lem  48369  clintopval  48680  1arymaptfo  49119  2arymptfv  49126  2arymaptfo  49130  ackval42  49172