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=A\to \left(xBy\leftrightarrow ABy\right)$$
2	1	exbidv	$$⊢x=A\to \left(\exists yxBy\leftrightarrow \exists yABy\right)$$
3		df-dm	$$⊢\mathrm{dom}B=\left\{x|\exists yxBy\right\}$$
4	2 3	elab2g	$$⊢A\in V\to \left(A\in \mathrm{dom}B\leftrightarrow \exists yABy\right)$$