MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reldmmpt2 Structured version   Unicode version

Theorem reldmmpt2 6412
Description: The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.)
Hypothesis
Ref Expression
rngop.1  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
Assertion
Ref Expression
reldmmpt2  |-  Rel  dom  F
Distinct variable groups:    y, A    x, y
Allowed substitution hints:    A( x)    B( x, y)    C( x, y)    F( x, y)

Proof of Theorem reldmmpt2
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 reldmoprab 6386 . 2  |-  Rel  dom  {
<. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
2 rngop.1 . . . . 5  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
3 df-mpt2 6301 . . . . 5  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
42, 3eqtri 2449 . . . 4  |-  F  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
54dmeqi 5047 . . 3  |-  dom  F  =  dom  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
65releqi 4929 . 2  |-  ( Rel 
dom  F  <->  Rel  dom  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) } )
71, 6mpbir 212 1  |-  Rel  dom  F
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370    = wceq 1437    e. wcel 1867   dom cdm 4845   Rel wrel 4850   {coprab 6297    |-> cmpt2 6298
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418  df-opab 4476  df-xp 4851  df-rel 4852  df-dm 4855  df-oprab 6300  df-mpt2 6301
This theorem is referenced by:  reldmmap  7480  reldmsets  15104  reldmress  15135  reldmprds  15307  gsum0  16473  reldmghm  16834  oppglsm  17235  reldmdprd  17570  reldmlmhm  18189  reldmpsr  18526  reldmmpl  18592  reldmopsr  18638  reldmevls  18681  vr1val  18726  reldmevls1  18847  evl1fval  18857  zrhval  19016  reldmdsmm  19233  frlmrcl  19257  matbas0pc  19371  mdetfval  19548  madufval  19599  qtopres  20650  fgabs  20831  reldmtng  21583  reldmnghm  21654  reldmnmhm  21655  dvbsss  22764  reldmmdeg  22913  reldmresv  28469  mzpmfp  35342
  Copyright terms: Public domain W3C validator