Theorem eldmg

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

	Ref	Expression
Assertion	eldmg	$$⊢A\in V\to \left(A\in \mathrm{dom}B\leftrightarrow \exists yABy\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢x=w\to \left(xBy\leftrightarrow wBy\right)$$
2	1	exbidv	$$⊢x=w\to \left(\exists yxBy\leftrightarrow \exists ywBy\right)$$
3		breq1	$$⊢w=A\to \left(wBy\leftrightarrow ABy\right)$$
4	3	exbidv	$$⊢w=A\to \left(\exists ywBy\leftrightarrow \exists yABy\right)$$
5		df-dm	$$⊢\mathrm{dom}B=\left\{x|\exists yxBy\right\}$$
6	2 4 5	elab2gw	$$⊢A\in V\to \left(A\in \mathrm{dom}B\leftrightarrow \exists yABy\right)$$