Metamath Proof Explorer

Theorem eldmres3

Description: Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 23-Nov-2025)

Ref Expression
Assertion eldmres3 ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A ↔ B ∈ A ∧ B R ≠ ∅

Proof

Step Hyp Ref Expression
1 eldmres2 ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A ↔ B ∈ A ∧ ∃ y y ∈ B R
2 n0 ⊢ B R ≠ ∅ ↔ ∃ y y ∈ B R
3 2 anbi2i ⊢ B ∈ A ∧ B R ≠ ∅ ↔ B ∈ A ∧ ∃ y y ∈ B R
4 1 3 bitr4di ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A ↔ B ∈ A ∧ B R ≠ ∅