![]() |
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 5992 and
brrelex1 5731.
Remark: there are many pairs like bj-opelresdm 36624 / bj-brresdm 36625, where one uses membership of ordered pairs and the other, related classes (for instance, bj-opelresdm 36624 / brrelex12 5730 or the opelopabg 5540 / brabg 5541 family). They are straightforwardly equivalent by df-br 5149. 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 5149 | . 2 ⊢ (𝐴(𝑅 ↾ 𝑋)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝑅 ↾ 𝑋)) | |
2 | bj-opelresdm 36624 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝑅 ↾ 𝑋) → 𝐴 ∈ 𝑋) | |
3 | 1, 2 | sylbi 216 | 1 ⊢ (𝐴(𝑅 ↾ 𝑋)𝐵 → 𝐴 ∈ 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2099 〈cop 4635 class class class wbr 5148 ↾ cres 5680 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-sep 5299 ax-nul 5306 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5149 df-opab 5211 df-xp 5684 df-res 5690 |
This theorem is referenced by: bj-idreseq 36641 |
Copyright terms: Public domain | W3C validator |