Metamath Proof Explorer


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 𝑅 ↔ ∃ 𝑦 𝑦 ∈ [ 𝐴 ] 𝑅 ) )