Theorem fvmptd2 6950

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

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

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 2709  ax-sep 5231  ax-pr 5370

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  updjudhcoinlf  9847  updjudhcoinrg  9848  lcmf0val  16582  fvprmselelfz  17006  fvprmselgcd1  17007  setcval  18035  catcval  18058  estrcval  18081  hofval  18209  yonval  18218  frmdval  18810  smndex1igid  18865  smndex1igidOLD  18866  smndex1n0mnd  18874  gexval  19544  rngcval  20586  ringcval  20615  frobrhm  21565  pmatcollpw3fi1lem1  22761  chfacfscmul0  22833  chfacfscmulgsum  22835  chfacfpmmul0  22837  chfacfpmmulgsum  22839  lmfval  23207  kgenval  23510  ptval  23545  utopval  24207  ustuqtoplem  24214  utopsnneiplem  24222  tusval  24240  blfvalps  24358  tmsval  24456  metuval  24524  caufval  25252  dchrval  27211  gausslemma2dlem2  27344  gausslemma2dlem3  27345  israg  28779  perpln1  28792  perpln2  28793  isperp  28794  vtxdgfval  29551  crctcsh  29907  clwlkclwwlklem2fv1  30080  clwlkclwwlklem2fv2  30081  cofmpt2  32722  pwrssmgc  33075  gsumfs2d  33137  elrgspnlem2  33319  elrgspnlem3  33320  elrgspnlem4  33321  rlocf1  33349  fracval  33380  qusima  33483  elrspunidl  33503  elrspunsn  33504  zringfrac  33629  r1pquslmic  33686  mplvrpmmhm  33705  mplvrpmrhm  33706  psrmonprod  33711  esplyfvaln  33733  fldextrspunlsp  33834  constrsuc  33898  madjusmdetlem2  33988  metidval  34050  pstmval  34055  carsgval  34463  dfttc3gw  36721  bj-rdg0gALT  37394  bj-finsumval0  37615  cdleme31fv2  40853  fiabv  42995  iunrelexpmin1  44153  iunrelexpmin2  44157  rfovcnvf1od  44449  limsup10exlem  46218  dvnprodlem1  46392  prproropf1olem3  47977  prprval  47986  isuspgrim0lem  48381  clintopval  48692  1arymaptfo  49131  2arymptfv  49138  2arymaptfo  49142  ackval42  49184