This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eldmressnALTV

Description: Element of the domain of a restriction to a singleton. (Contributed by Peter Mazsa, 12-Jun-2024)

Ref Expression
Assertion eldmressnALTV ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ { 𝐴 } ) ↔ ( 𝐵 = 𝐴 ∧ 𝐴 ∈ dom 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 eldmres ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ { 𝐴 } ) ↔ ( 𝐵 ∈ { 𝐴 } ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ) )
2 elsng ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ { 𝐴 } ↔ 𝐵 = 𝐴 ) )
3 eldmg ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom 𝑅 ↔ ∃ 𝑦 𝐵 𝑅 𝑦 ) )
4 3 bicomd ⊢ ( 𝐵 ∈ 𝑉 → ( ∃ 𝑦 𝐵 𝑅 𝑦 ↔ 𝐵 ∈ dom 𝑅 ) )
5 2 4 anbi12d ⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝐵 ∈ { 𝐴 } ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ↔ ( 𝐵 = 𝐴 ∧ 𝐵 ∈ dom 𝑅 ) ) )
6 1 5 bitrd ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ { 𝐴 } ) ↔ ( 𝐵 = 𝐴 ∧ 𝐵 ∈ dom 𝑅 ) ) )
7 eqelb ⊢ ( ( 𝐵 = 𝐴 ∧ 𝐵 ∈ dom 𝑅 ) ↔ ( 𝐵 = 𝐴 ∧ 𝐴 ∈ dom 𝑅 ) )
8 6 7 bitrdi ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ { 𝐴 } ) ↔ ( 𝐵 = 𝐴 ∧ 𝐴 ∈ dom 𝑅 ) ) )