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

Theorem mpofun 7534
Description: The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.) (Proof shortened by SN, 23-Jul-2024.)
Hypothesis
Ref Expression
mpofun.1 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
Assertion
Ref Expression
mpofun Fun 𝐹
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem mpofun
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 moeq 3703 . . . 4 ∃*𝑧 𝑧 = 𝐶
21moani 2547 . . 3 ∃*𝑧((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
32funoprab 7532 . 2 Fun {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
4 mpofun.1 . . . 4 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
5 df-mpo 7416 . . . 4 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
64, 5eqtri 2760 . . 3 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
76funeqi 6569 . 2 (Fun 𝐹 ↔ Fun {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)})
83, 7mpbir 230 1 Fun 𝐹
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1541  wcel 2106  Fun wfun 6537  {coprab 7412  cmpo 7413
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 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-fun 6545  df-oprab 7415  df-mpo 7416
This theorem is referenced by:  ofexg  7677  mpoexxg  8064  mpoexw  8067  mpocurryd  8256  imasvscafn  17487  coapm  18025  oppglsm  19551  gsum2d2lem  19882  evlslem2  21861  xkococnlem  23383  ucnima  24006  ucnprima  24007  fmucnd  24017  scutf  27538  smatrcl  33062  smatlem  33063  txomap  33100  tpr2rico  33178  elunirnmbfm  33536  relowlpssretop  36548  aovmpt4g  46208  mpoexxg2  47102
  Copyright terms: Public domain W3C validator