Metamath Proof Explorer

Theorem eldmxrncnvepres

Description: Element of the domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025)

Ref Expression
Assertion eldmxrncnvepres ⊢ B ∈ V → B ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ B ∈ A ∧ B ≠ ∅ ∧ B R ≠ ∅

Proof

Step Hyp Ref Expression
1 eldmres3 ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A ↔ B ∈ A ∧ B R ≠ ∅
2 1 anbi1d ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A ∧ B ≠ ∅ ↔ B ∈ A ∧ B R ≠ ∅ ∧ B ≠ ∅
3 dmxrncnvepres ⊢ dom ⁡ R ⋉ E -1 ↾ A = dom ⁡ R ↾ A ∖ ∅
4 3 eleq2i ⊢ B ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ B ∈ dom ⁡ R ↾ A ∖ ∅
5 eldifsn ⊢ B ∈ dom ⁡ R ↾ A ∖ ∅ ↔ B ∈ dom ⁡ R ↾ A ∧ B ≠ ∅
6 4 5 bitri ⊢ B ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ B ∈ dom ⁡ R ↾ A ∧ B ≠ ∅
7 3anan32 ⊢ B ∈ A ∧ B ≠ ∅ ∧ B R ≠ ∅ ↔ B ∈ A ∧ B R ≠ ∅ ∧ B ≠ ∅
8 2 6 7 3bitr4g ⊢ B ∈ V → B ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ B ∈ A ∧ B ≠ ∅ ∧ B R ≠ ∅