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