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

Theorem mpofun 7528
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 3702 . . . 4 ∃*𝑧 𝑧 = 𝐶
21moani 2547 . . 3 ∃*𝑧((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
32funoprab 7526 . 2 Fun {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
4 mpofun.1 . . . 4 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
5 df-mpo 7410 . . . 4 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
64, 5eqtri 2760 . . 3 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
76funeqi 6566 . 2 (Fun 𝐹 ↔ Fun {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)})
83, 7mpbir 230 1 Fun 𝐹
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1541  wcel 2106  Fun wfun 6534  {coprab 7406  cmpo 7407
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 5298  ax-nul 5305  ax-pr 5426
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 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-fun 6542  df-oprab 7409  df-mpo 7410
This theorem is referenced by:  ofexg  7671  mpoexxg  8058  mpoexw  8061  mpocurryd  8250  imasvscafn  17479  coapm  18017  oppglsm  19504  gsum2d2lem  19835  evlslem2  21633  xkococnlem  23154  ucnima  23777  ucnprima  23778  fmucnd  23788  scutf  27302  smatrcl  32764  smatlem  32765  txomap  32802  tpr2rico  32880  elunirnmbfm  33238  relowlpssretop  36233  aovmpt4g  45895  mpoexxg2  46966
  Copyright terms: Public domain W3C validator