Theorem fvmptd2 6994

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5186  ‘cfv 6531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6487  df-fun 6533  df-fv 6539

This theorem is used by:  updjudhcoinlf  9994  updjudhcoinrg  9995  lcmf0val  16777  fvprmselelfz  17202  fvprmselgcd1  17203  setcval  18232  catcval  18255  estrcval  18278  hofval  18406  yonval  18415  frmdval  19027  smndex1igid  19082  smndex1igidOLD  19083  smndex1n0mnd  19091  gexval  19772  rngcval  20850  ringcval  20879  frobrhm  21861  pmatcollpw3fi1lem1  23084  chfacfscmul0  23156  chfacfscmulgsum  23158  chfacfpmmul0  23160  chfacfpmmulgsum  23162  lmfval  23530  kgenval  23834  ptval  23869  utopval  24531  ustuqtoplem  24538  utopsnneiplem  24546  tusval  24564  blfvalps  24682  tmsval  24780  metuval  24848  caufval  25576  dchrval  27543  gausslemma2dlem2  27676  gausslemma2dlem3  27677  israg  29154  perpln1  29167  perpln2  29168  isperp  29169  vtxdgfval  30030  crctcsh  30395  clwlkclwwlklem2fv1  30568  clwlkclwwlklem2fv2  30569  cofmpt2  33210  pwrssmgc  33543  gsumfs2d  33604  elrgspnlem2  33786  elrgspnlem3  33787  elrgspnlem4  33788  rlocf1  33817  fracval  33848  qusima  33941  elrspunidl  33960  elrspunsn  33961  zringfrac  34068  r1pquslmic  34124  0mplrim  34128  selvply1rhmlemb  34133  selvply1rhmlem2  34135  selvply1rhmlem4  34137  mplvrpmmhm  34160  mplvrpmrhm  34161  psrmonprod  34166  esplyfvaln  34188  fldextrspunlsp  34288  constrsuc  34352  madjusmdetlem2  34442  metidval  34504  pstmval  34509  carsgval  34918  dfttc3gw  37281  bj-rdg0gALT  37954  bj-finsumval0  38174  cdleme31fv2  41418  fiabv  43562  iunrelexpmin1  44667  iunrelexpmin2  44671  rfovcnvf1od  44963  limsup10exlem  46726  dvnprodlem1  46900  prproropf1olem3  48531  prprval  48540  isuspgrim0lem  48935  clintopval  49245  1arymaptfo  49699  2arymptfv  49706  2arymaptfo  49710  ackval42  49752