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

Theorem mptfvmpt 7104
Description: A function in maps-to notation as the value of another function in maps-to notation. (Contributed by AV, 20-Aug-2022.)
Hypotheses
Ref Expression
mptfvmpt.y (𝑦 = 𝑌𝑀 = (𝑥𝑉𝐴))
mptfvmpt.g 𝐺 = (𝑦𝑊𝑀)
mptfvmpt.v 𝑉 = (𝐹𝑋)
Assertion
Ref Expression
mptfvmpt (𝑌𝑊 → (𝐺𝑌) = (𝑥𝑉𝐴))
Distinct variable groups:   𝑦,𝐴   𝑥,𝑉,𝑦   𝑦,𝑊   𝑦,𝑌
Allowed substitution hints:   𝐴(𝑥)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)   𝑀(𝑥,𝑦)   𝑊(𝑥)   𝑋(𝑥,𝑦)   𝑌(𝑥)

Proof of Theorem mptfvmpt
StepHypRef Expression
1 mptfvmpt.y . 2 (𝑦 = 𝑌𝑀 = (𝑥𝑉𝐴))
2 mptfvmpt.g . 2 𝐺 = (𝑦𝑊𝑀)
3 mptfvmpt.v . . . 4 𝑉 = (𝐹𝑋)
43fvexi 6788 . . 3 𝑉 ∈ V
54mptex 7099 . 2 (𝑥𝑉𝐴) ∈ V
61, 2, 5fvmpt 6875 1 (𝑌𝑊 → (𝐺𝑌) = (𝑥𝑉𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wcel 2106  cmpt 5157  cfv 6433
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441
This theorem is referenced by:  cidfval  17385  idafval  17772  grpinvfvalALT  18619  grplactfval  18676  odfvalALT  19141  asclfval  21083  ig1pval  25337  ishlg  26963  htthlem  29279  sgnsv  31427  mvrsval  33467  mvhfval  33495  msrfval  33499  lkrfval  37101  pmapfval  37770  watfvalN  38006  ldilfset  38122  ltrnfset  38131  dilfsetN  38166  trnfsetN  38169  trlfset  38174  tgrpfset  38758  tendofset  38772  tendoi  38808  erngfset  38813  erngfset-rN  38821  dvafset  39018  diaffval  39044  dvhfset  39094  docaffvalN  39135  djaffvalN  39147  dibffval  39154  dicffval  39188  dihffval  39244  dihfval  39245  dochffval  39363  djhffval  39410  lcfrlem8  39563  lcdfval  39602  mapdffval  39640  mapdfval  39641  hvmapffval  39772  hdmap1ffval  39809  hdmapffval  39840  hdmapfval  39841  hgmapffval  39899  hgmapfval  39900  hbtlem1  40948  hbtlem7  40950
  Copyright terms: Public domain W3C validator