Metamath Proof Explorer

Theorem eldmres2

Description: Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 21-Aug-2020)

Ref Expression
Assertion eldmres2 ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A ↔ B ∈ A ∧ ∃ y y ∈ B R

Proof

Step Hyp Ref Expression
1 eldmres ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A ↔ B ∈ A ∧ ∃ y B R y
2 eldmg ⊢ B ∈ V → B ∈ dom ⁡ R ↔ ∃ y B R y
3 eldm4 ⊢ B ∈ V → B ∈ dom ⁡ R ↔ ∃ y y ∈ B R
4 2 3 bitr3d ⊢ B ∈ V → ∃ y B R y ↔ ∃ y y ∈ B R
5 4 anbi2d ⊢ B ∈ V → B ∈ A ∧ ∃ y B R y ↔ B ∈ A ∧ ∃ y y ∈ B R
6 1 5 bitrd ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A ↔ B ∈ A ∧ ∃ y y ∈ B R