Metamath Proof Explorer

Theorem eldmres

Description: Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 9-Jan-2019)

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

Proof

Step Hyp Ref Expression
1 eldmg ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A ↔ ∃ y B R ↾ A y
2 brres ⊢ y ∈ V → B R ↾ A y ↔ B ∈ A ∧ B R y
3 2 elv ⊢ B R ↾ A y ↔ B ∈ A ∧ B R y
4 3 exbii ⊢ ∃ y B R ↾ A y ↔ ∃ y B ∈ A ∧ B R y
5 19.42v ⊢ ∃ y B ∈ A ∧ B R y ↔ B ∈ A ∧ ∃ y B R y
6 4 5 bitri ⊢ ∃ y B R ↾ A y ↔ B ∈ A ∧ ∃ y B R y
7 1 6 bitrdi ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A ↔ B ∈ A ∧ ∃ y B R y