Metamath Proof Explorer

Theorem eldmxrncnvepres

Description: Element of the domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025)

Ref Expression
Assertion eldmxrncnvepres 
|- ( B e. V -> ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. A /\ B =/= (/) /\ [ B ] R =/= (/) ) ) )

Proof

Step Hyp Ref Expression
1 eldmres3 
 |-  ( B e. V -> ( B e. dom ( R |` A ) <-> ( B e. A /\ [ B ] R =/= (/) ) ) )
2 1 anbi1d 
 |-  ( B e. V -> ( ( B e. dom ( R |` A ) /\ B =/= (/) ) <-> ( ( B e. A /\ [ B ] R =/= (/) ) /\ B =/= (/) ) ) )
3 dmxrncnvepres 
 |-  dom ( R |X. ( `' _E |` A ) ) = ( dom ( R |` A ) \ { (/) } )
4 3 eleq2i 
 |-  ( B e. dom ( R |X. ( `' _E |` A ) ) <-> B e. ( dom ( R |` A ) \ { (/) } ) )
5 eldifsn 
 |-  ( B e. ( dom ( R |` A ) \ { (/) } ) <-> ( B e. dom ( R |` A ) /\ B =/= (/) ) )
6 4 5 bitri 
 |-  ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. dom ( R |` A ) /\ B =/= (/) ) )
7 3anan32 
 |-  ( ( B e. A /\ B =/= (/) /\ [ B ] R =/= (/) ) <-> ( ( B e. A /\ [ B ] R =/= (/) ) /\ B =/= (/) ) )
8 2 6 7 3bitr4g 
 |-  ( B e. V -> ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. A /\ B =/= (/) /\ [ B ] R =/= (/) ) ) )