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

Theorem reldmress 14312
Description: The structure restriction is a proper operator, so it can be used with ovprc1 6204. (Contributed by Stefan O'Rear, 29-Nov-2014.)
Assertion
Ref Expression
reldmress  |-  Rel  doms

Proof of Theorem reldmress
Dummy variables  w  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ress 14269 . 2  |-s  =  ( w  e.  _V ,  a  e. 
_V  |->  if ( (
Base `  w )  C_  a ,  w ,  ( w sSet  <. ( Base `  ndx ) ,  ( a  i^i  ( Base `  w ) )
>. ) ) )
21reldmmpt2 6287 1  |-  Rel  doms
Colors of variables: wff setvar class
Syntax hints:   _Vcvv 3054    i^i cin 3411    C_ wss 3412   ifcif 3875   <.cop 3967   dom cdm 4924   Rel wrel 4929   ` cfv 5502  (class class class)co 6176   ndxcnx 14259   sSet csts 14260   Basecbs 14262   ↾s cress 14263
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 1709  ax-7 1729  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4497  ax-nul 4505  ax-pr 4615
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 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3056  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-nul 3722  df-if 3876  df-sn 3962  df-pr 3964  df-op 3968  df-br 4377  df-opab 4435  df-xp 4930  df-rel 4931  df-dm 4934  df-oprab 6180  df-mpt2 6181  df-ress 14269
This theorem is referenced by:  ressbas  14316  ressbasss  14318  resslem  14319  ress0  14320  ressinbas  14322  ressress  14323  wunress  14325  subcmn  16411  srasca  17354  rlmsca2  17374  resstopn  18892  cphsubrglem  20798  submomnd  26293  suborng  26403
  Copyright terms: Public domain W3C validator