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\in V\to \left(A\in \mathrm{dom}B\leftrightarrow \exists y⟨A,y⟩\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldmg	$$⊢A\in V\to \left(A\in \mathrm{dom}B\leftrightarrow \exists yABy\right)$$
2		df-br	$$⊢ABy\leftrightarrow ⟨A,y⟩\in B$$
3	2	exbii	$$⊢\exists yABy\leftrightarrow \exists y⟨A,y⟩\in B$$
4	1 3	bitrdi	$$⊢A\in V\to \left(A\in \mathrm{dom}B\leftrightarrow \exists y⟨A,y⟩\in B\right)$$