![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reldmress | Structured version Visualization version GIF version |
Description: The structure restriction is a proper operator, so it can be used with ovprc1 7458. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
Ref | Expression |
---|---|
reldmress | ⊢ Rel dom ↾s |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ress 17213 | . 2 ⊢ ↾s = (𝑤 ∈ V, 𝑎 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑎, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑎 ∩ (Base‘𝑤))〉))) | |
2 | 1 | reldmmpo 7555 | 1 ⊢ Rel dom ↾s |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3461 ∩ cin 3943 ⊆ wss 3944 ifcif 4530 〈cop 4636 dom cdm 5678 Rel wrel 5683 ‘cfv 6549 (class class class)co 7419 sSet csts 17135 ndxcnx 17165 Basecbs 17183 ↾s cress 17212 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 df-opab 5212 df-xp 5684 df-rel 5685 df-dm 5688 df-oprab 7423 df-mpo 7424 df-ress 17213 |
This theorem is referenced by: ressbas 17218 ressbasOLD 17219 ressbasssg 17220 ressbasssOLD 17223 resseqnbas 17225 resslemOLD 17226 ress0 17227 ressinbas 17229 ressress 17232 wunress 17234 wunressOLD 17235 subcmn 19804 srasca 21081 srascaOLD 21082 rlmsca2 21104 resstopn 23134 cphsubrglem 25149 submomnd 32880 suborng 33129 |
Copyright terms: Public domain | W3C validator |