MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvmptd2 Structured version   Visualization version   GIF version

Theorem fvmptd2 6956
Description: Deduction version of fvmpt 6948 (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
StepHypRef Expression
1 fvmptd2.1 . . 3 𝐹 = (𝑥𝐷𝐵)
21a1i 11 . 2 (𝜑𝐹 = (𝑥𝐷𝐵))
3 fvmptd2.2 . 2 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
4 fvmptd2.3 . 2 (𝜑𝐴𝐷)
5 fvmptd2.4 . 2 (𝜑𝐶𝑉)
62, 3, 4, 5fvmptd 6955 1 (𝜑 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  cmpt 5188  cfv 6496
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-iota 6448  df-fun 6498  df-fv 6504
This theorem is referenced by:  fvmptopabOLD  7411  updjudhcoinlf  9867  updjudhcoinrg  9868  lcmf0val  16497  fvprmselelfz  16915  fvprmselgcd1  16916  setcval  17962  catcval  17985  estrcval  18010  hofval  18140  yonval  18149  frmdval  18660  smndex1igid  18713  smndex1n0mnd  18721  gexval  19358  pmatcollpw3fi1lem1  22133  chfacfscmul0  22205  chfacfscmulgsum  22207  chfacfpmmul0  22209  chfacfpmmulgsum  22211  lmfval  22581  kgenval  22884  ptval  22919  utopval  23582  ustuqtoplem  23589  utopsnneiplem  23597  tusval  23615  blfvalps  23734  tmsval  23834  metuval  23903  caufval  24637  dchrval  26580  gausslemma2dlem2  26713  gausslemma2dlem3  26714  israg  27586  perpln1  27599  perpln2  27600  isperp  27601  vtxdgfval  28362  crctcsh  28716  clwlkclwwlklem2fv1  28886  clwlkclwwlklem2fv2  28887  cofmpt2  31495  pwrssmgc  31804  frobrhm  32012  qusima  32131  elrspunidl  32143  metidval  32411  pstmval  32416  carsgval  32843  bj-rdg0gALT  35532  bj-finsumval0  35746  cdleme31fv2  38846  iunrelexpmin1  41961  iunrelexpmin2  41965  rfovcnvf1od  42257  limsup10exlem  43984  prproropf1olem3  45668  prprval  45677  clintopval  46109  rngcval  46231  ringcval  46277  1arymaptfo  46700  2arymptfv  46707  2arymaptfo  46711  ackval42  46753
  Copyright terms: Public domain W3C validator