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 𝑅 ) ) )