Metamath Proof Explorer


Theorem eldm2g

Description: Domain membership. Theorem 4 of Suppes p. 59. (Contributed by NM, 27-Jan-1997) (Revised by Mario Carneiro, 9-Jul-2014)

Ref Expression
Assertion eldm2g A V A dom B y A y B

Proof

Step Hyp Ref Expression
1 eldmg A V A dom B y A B y
2 df-br A B y A y B
3 2 exbii y A B y y A y B
4 1 3 bitrdi A V A dom B y A y B