This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opres

Description: Ordered pair membership in a restriction when the first member belongs to the restricting class. (Contributed by NM, 30-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Hypothesis opres.1 ⊢ B ∈ V
Assertion opres ⊢ A ∈ D → A B ∈ C ↾ D ↔ A B ∈ C

Proof

Step Hyp Ref Expression
1 opres.1 ⊢ B ∈ V
2 1 opelresi ⊢ A B ∈ C ↾ D ↔ A ∈ D ∧ A B ∈ C
3 2 baib ⊢ A ∈ D → A B ∈ C ↾ D ↔ A B ∈ C