Metamath Proof Explorer

Theorem eldm1cossres2

Description: Elementhood in the domain of restricted cosets. (Contributed by Peter Mazsa, 30-Dec-2018)

Ref Expression
Assertion eldm1cossres2 ⊢ B ∈ V → B ∈ dom ⁡ ≀ R ↾ A ↔ ∃ x ∈ A B ∈ x R

Proof

Step Hyp Ref Expression
1 eldm1cossres ⊢ B ∈ V → B ∈ dom ⁡ ≀ R ↾ A ↔ ∃ x ∈ A x R B
2 elecALTV ⊢ x ∈ V ∧ B ∈ V → B ∈ x R ↔ x R B
3 2 el2v1 ⊢ B ∈ V → B ∈ x R ↔ x R B
4 3 rexbidv ⊢ B ∈ V → ∃ x ∈ A B ∈ x R ↔ ∃ x ∈ A x R B
5 1 4 bitr4d ⊢ B ∈ V → B ∈ dom ⁡ ≀ R ↾ A ↔ ∃ x ∈ A B ∈ x R