**Description:** If an ordered pair is in a restricted binary relation, then its first
component is an element of the restricting class. See also opelres .
(Contributed by BJ, 25-Dec-2023)

Ref | Expression | ||
---|---|---|---|

Assertion | bj-opelresdm | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 ↾ 𝑋 ) → 𝐴 ∈ 𝑋 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | elin | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 ∩ ( 𝑋 × V ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × V ) ) ) | |

2 | opelxp1 | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × V ) → 𝐴 ∈ 𝑋 ) | |

3 | 1 2 | simplbiim | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 ∩ ( 𝑋 × V ) ) → 𝐴 ∈ 𝑋 ) |

4 | df-res | ⊢ ( 𝑅 ↾ 𝑋 ) = ( 𝑅 ∩ ( 𝑋 × V ) ) | |

5 | 3 4 | eleq2s | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 ↾ 𝑋 ) → 𝐴 ∈ 𝑋 ) |