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	⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐴 ⟩ ∈ ( I ↾ 𝐵 ) ↔ 𝐴 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ididg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 I 𝐴 )
2		df-br	⊢ ( 𝐴 I 𝐴 ↔ ⟨ 𝐴 , 𝐴 ⟩ ∈ I )
3	1 2	sylib	⊢ ( 𝐴 ∈ 𝑉 → ⟨ 𝐴 , 𝐴 ⟩ ∈ I )
4		opelres	⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐴 ⟩ ∈ ( I ↾ 𝐵 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ⟨ 𝐴 , 𝐴 ⟩ ∈ I ) ) )
5	3 4	mpbiran2d	⊢ ( 𝐴 ∈ 𝑉 → ( ⟨ 𝐴 , 𝐴 ⟩ ∈ ( I ↾ 𝐵 ) ↔ 𝐴 ∈ 𝐵 ) )