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

Theorem reldmmpt2 6314
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 6288 . 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 6208 . . . . 5  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
42, 3eqtri 2483 . . . 4  |-  F  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
54dmeqi 5152 . . 3  |-  dom  F  =  dom  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
65releqi 5034 . 2  |-  ( Rel 
dom  F  <->  Rel  dom  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) } )
71, 6mpbir 209 1  |-  Rel  dom  F
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1370    e. wcel 1758   dom cdm 4951   Rel wrel 4956   {coprab 6204    |-> cmpt2 6205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-br 4404  df-opab 4462  df-xp 4957  df-rel 4958  df-dm 4961  df-oprab 6207  df-mpt2 6208
This theorem is referenced by:  bropopvvv  6766  supp0prc  6806  reldmmap  7336  reldmsets  14317  reldmress  14346  reldmprds  14509  gsum0  15632  reldmghm  15868  oppglsm  16265  reldmdprd  16604  reldmlmhm  17232  reldmpsr  17554  reldmmpl  17627  reldmopsr  17682  reldmevls  17730  vr1val  17775  reldmevls1  17880  evl1fval  17890  zrhval  18067  reldmdsmm  18286  frlmrcl  18312  matbas0pc  18414  submafval  18520  mdetfval  18527  madufval  18578  qtopres  19406  fgabs  19587  reldmtng  20359  reldmnghm  20426  reldmnmhm  20427  dvbsss  21513  reldmmdeg  21662  reldmresv  26459  mzpmfp  29251  mzpmfpOLD  29252  clwwlknprop  30603
  Copyright terms: Public domain W3C validator