Metamath Proof Explorer


Theorem eldmg

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

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

Proof

Step Hyp Ref Expression
1 breq1 x = A x B y A B y
2 1 exbidv x = A y x B y y A B y
3 df-dm dom B = x | y x B y
4 2 3 elab2g A V A dom B y A B y