Theorem eldm4

Description: Elementhood in a domain. (Contributed by Peter Mazsa, 24-Oct-2018)

	Ref	Expression
Assertion	eldm4	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑦 𝑦 ∈ [ 𝐴 ] 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eldmg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑦 𝐴 𝑅 𝑦 ) )
2		elecALTV	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ V ) → ( 𝑦 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑦 ) )
3	2	elvd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑦 ) )
4	3	exbidv	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑦 𝑦 ∈ [ 𝐴 ] 𝑅 ↔ ∃ 𝑦 𝐴 𝑅 𝑦 ) )
5	1 4	bitr4d	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑦 𝑦 ∈ [ 𝐴 ] 𝑅 ) )