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