Theorem eldmressnALTV

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

	Ref	Expression
Assertion	eldmressnALTV	|- ( B e. V -> ( B e. dom ( R |` { A } ) <-> ( B = A /\ A e. dom R ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldmres	|- ( B e. V -> ( B e. dom ( R |` { A } ) <-> ( B e. { A } /\ E. y B R y ) ) )
2		elsng	|- ( B e. V -> ( B e. { A } <-> B = A ) )
3		eldmg	|- ( B e. V -> ( B e. dom R <-> E. y B R y ) )
4	3	bicomd	|- ( B e. V -> ( E. y B R y <-> B e. dom R ) )
5	2 4	anbi12d	|- ( B e. V -> ( ( B e. { A } /\ E. y B R y ) <-> ( B = A /\ B e. dom R ) ) )
6	1 5	bitrd	|- ( B e. V -> ( B e. dom ( R |` { A } ) <-> ( B = A /\ B e. dom R ) ) )
7		eqelb	|- ( ( B = A /\ B e. dom R ) <-> ( B = A /\ A e. dom R ) )
8	6 7	bitrdi	|- ( B e. V -> ( B e. dom ( R |` { A } ) <-> ( B = A /\ A e. dom R ) ) )