Metamath Proof Explorer


Theorem eldmres

Description: Elementhood in the domain of a restriction. (Contributed by Peter Mazsa, 9-Jan-2019)

Ref Expression
Assertion eldmres B V B dom R A B A y B R y

Proof

Step Hyp Ref Expression
1 eldmg B V B dom R A y B R A y
2 brres y V B R A y B A B R y
3 2 elv B R A y B A B R y
4 3 exbii y B R A y y B A B R y
5 19.42v y B A B R y B A y B R y
6 4 5 bitri y B R A y B A y B R y
7 1 6 bitrdi B V B dom R A B A y B R y