Metamath Proof Explorer

Theorem opelresi

Description: Ordered pair membership in a restriction. Exercise 13 of TakeutiZaring p. 25. (Contributed by NM, 13-Nov-1995)

Ref Expression
Hypothesis opelresi.1 ⊢ C ∈ V
Assertion opelresi ⊢ B C ∈ R ↾ A ↔ B ∈ A ∧ B C ∈ R

Proof

Step Hyp Ref Expression
1 opelresi.1 ⊢ C ∈ V
2 opelres ⊢ C ∈ V → B C ∈ R ↾ A ↔ B ∈ A ∧ B C ∈ R
3 1 2 ax-mp ⊢ B C ∈ R ↾ A ↔ B ∈ A ∧ B C ∈ R