Theorem bj-brresdm 37197

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 5940 and brrelex1 5672.

Remark: there are many pairs like bj-opelresdm 37196 / bj-brresdm 37197, where one uses membership of ordered pairs and the other, related classes (for instance, bj-opelresdm 37196 / brrelex12 5671 or the opelopabg 5481 / brabg 5482 family). They are straightforwardly equivalent by df-br 5094. 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.)

Assertion

Ref	Expression
bj-brresdm	⊢ (𝐴(𝑅 ↾ 𝑋)𝐵 → 𝐴 ∈ 𝑋)

Proof of Theorem bj-brresdm

Step	Hyp	Ref	Expression
1		df-br 5094	. 2 ⊢ (𝐴(𝑅 ↾ 𝑋)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝑅 ↾ 𝑋))
2		bj-opelresdm 37196	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑅 ↾ 𝑋) → 𝐴 ∈ 𝑋)
3	1, 2	sylbi 217	1 ⊢ (𝐴(𝑅 ↾ 𝑋)𝐵 → 𝐴 ∈ 𝑋)

Syntax hints:   → wi 4   ∈ wcel 2111  ⟨cop 4581   class class class wbr 5093   ↾ cres 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-xp 5625  df-res 5631

This theorem is referenced by:  bj-idreseq  37213