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

Metamath Proof Explorer

Theorem opelidres

Description: <. A , A >. belongs to a restriction of the identity class iff A belongs to the restricting class. (Contributed by FL, 27-Oct-2008) (Revised by NM, 30-Mar-2016)

Ref Expression
Assertion opelidres ⊢ A ∈ V → A A ∈ I ↾ B ↔ A ∈ B

Proof

Step Hyp Ref Expression
1 ididg ⊢ A ∈ V → A I A
2 df-br ⊢ A I A ↔ A A ∈ I
3 1 2 sylib ⊢ A ∈ V → A A ∈ I
4 opelres ⊢ A ∈ V → A A ∈ I ↾ B ↔ A ∈ B ∧ A A ∈ I
5 3 4 mpbiran2d ⊢ A ∈ V → A A ∈ I ↾ B ↔ A ∈ B