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

Theorem reldmmpt2 6042
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 6019 . 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 5950 . . . . 5  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
42, 3eqtri 2378 . . . 4  |-  F  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
54dmeqi 4962 . . 3  |-  dom  F  =  dom  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
65releqi 4854 . 2  |-  ( Rel 
dom  F  <->  Rel  dom  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) } )
71, 6mpbir 200 1  |-  Rel  dom  F
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1642    e. wcel 1710   dom cdm 4771   Rel wrel 4776   {coprab 5946    e. cmpt2 5947
This theorem is referenced by:  reldmmap  6869  reldmsets  13267  reldmress  13291  reldmprds  13448  gsum0  14556  reldmghm  14781  oppglsm  15052  reldmdprd  15334  reldmlmhm  15881  reldmpsr  16208  reldmmpl  16271  reldmopsr  16314  vr1val  16370  zrhval  16568  qtopres  17495  fgabs  17676  reldmtng  18256  reldmnghm  18323  reldmnmhm  18324  dvbsss  19356  reldmevls  19505  evlval  19512  evl1fval  19514  reldmmdeg  19547  mzpmfp  26148  reldmdsmm  26522  frlmrcl  26548  mdetfval  26810  bropopvvv  27435  brovex  27446
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pr 4295
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4105  df-opab 4159  df-xp 4777  df-rel 4778  df-dm 4781  df-oprab 5949  df-mpt2 5950
  Copyright terms: Public domain W3C validator