Metamath Proof Explorer

Theorem eldm1cossres

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

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

Proof

Step Hyp Ref Expression
1 eldmcoss ⊢ B ∈ V → B ∈ dom ⁡ ≀ R ↾ A ↔ ∃ u u R ↾ A B
2 brres ⊢ B ∈ V → u R ↾ A B ↔ u ∈ A ∧ u R B
3 2 exbidv ⊢ B ∈ V → ∃ u u R ↾ A B ↔ ∃ u u ∈ A ∧ u R B
4 1 3 bitrd ⊢ B ∈ V → B ∈ dom ⁡ ≀ R ↾ A ↔ ∃ u u ∈ A ∧ u R B
5 df-rex ⊢ ∃ u ∈ A u R B ↔ ∃ u u ∈ A ∧ u R B
6 4 5 bitr4di ⊢ B ∈ V → B ∈ dom ⁡ ≀ R ↾ A ↔ ∃ u ∈ A u R B