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

Theorem reldmmpt2 6404
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 6378 . 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 6293 . . . . 5  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
42, 3eqtri 2472 . . . 4  |-  F  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
54dmeqi 5035 . . 3  |-  dom  F  =  dom  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
65releqi 4917 . 2  |-  ( Rel 
dom  F  <->  Rel  dom  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) } )
71, 6mpbir 213 1  |-  Rel  dom  F
Colors of variables: wff setvar class
Syntax hints:    /\ wa 371    = wceq 1443    e. wcel 1886   dom cdm 4833   Rel wrel 4838   {coprab 6289    |-> cmpt2 6290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-opab 4461  df-xp 4839  df-rel 4840  df-dm 4843  df-oprab 6292  df-mpt2 6293
This theorem is referenced by:  reldmmap  7478  reldmsets  15137  reldmress  15168  reldmprds  15340  gsum0  16514  reldmghm  16875  oppglsm  17287  reldmdprd  17622  reldmlmhm  18241  reldmpsr  18578  reldmmpl  18644  reldmopsr  18690  reldmevls  18733  vr1val  18778  reldmevls1  18899  evl1fval  18909  zrhval  19072  reldmdsmm  19289  frlmrcl  19313  matbas0pc  19427  mdetfval  19604  madufval  19655  qtopres  20706  fgabs  20887  reldmtng  21639  reldmnghm  21710  reldmnmhm  21711  dvbsss  22850  reldmmdeg  22999  reldmresv  28582  mzpmfp  35583  nbgrprc0  39385
  Copyright terms: Public domain W3C validator