![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-brresdm | Structured version Visualization version GIF version |
Description: If two classes are
related by a restricted binary relation, then the first
class is an element of the restricting class. See also brres 5981 and
brrelex1 5722.
Remark: there are many pairs like bj-opelresdm 36533 / bj-brresdm 36534, where one uses membership of ordered pairs and the other, related classes (for instance, bj-opelresdm 36533 / brrelex12 5721 or the opelopabg 5531 / brabg 5532 family). They are straightforwardly equivalent by df-br 5142. The latter is indeed a very direct definition, introducing a "shorthand", and barely necessary, were it not for the frequency of the expression 𝐴𝑅𝐵. Therefore, in the spirit of "definitions are here to be used", most theorems, apart from the most elementary ones, should only have the "br" version, not the "opel" one. (Contributed by BJ, 25-Dec-2023.) |
Ref | Expression |
---|---|
bj-brresdm | ⊢ (𝐴(𝑅 ↾ 𝑋)𝐵 → 𝐴 ∈ 𝑋) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-br 5142 | . 2 ⊢ (𝐴(𝑅 ↾ 𝑋)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅 ↾ 𝑋)) | |
2 | bj-opelresdm 36533 | . 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ↾ 𝑋) → 𝐴 ∈ 𝑋) | |
3 | 1, 2 | sylbi 216 | 1 ⊢ (𝐴(𝑅 ↾ 𝑋)𝐵 → 𝐴 ∈ 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 ⟨cop 4629 class class class wbr 5141 ↾ cres 5671 |
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-ext 2697 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2704 df-cleq 2718 df-clel 2804 df-ral 3056 df-rex 3065 df-rab 3427 df-v 3470 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-nul 4318 df-if 4524 df-sn 4624 df-pr 4626 df-op 4630 df-br 5142 df-opab 5204 df-xp 5675 df-res 5681 |
This theorem is referenced by: bj-idreseq 36550 |
Copyright terms: Public domain | W3C validator |