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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom 𝐵 ↔ ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eldmg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom 𝐵 ↔ ∃ 𝑦 𝐴 𝐵 𝑦 ) )
2		df-br	⊢ ( 𝐴 𝐵 𝑦 ↔ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐵 )
3	2	exbii	⊢ ( ∃ 𝑦 𝐴 𝐵 𝑦 ↔ ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐵 )
4	1 3	bitrdi	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom 𝐵 ↔ ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐵 ) )