Theorem eldmxrncnvepres2

Description: Element of the domain of the range product with restricted converse epsilon relation. This identifies the domain of the pet span ( R |X. ( ' E | A ) ) : a B belongs to the domain of the span exactly when B is in A and has at least one x e. B and y with B R y . (Contributed by Peter Mazsa, 23-Nov-2025)

	Ref	Expression
Assertion	eldmxrncnvepres2	|- ( B e. V -> ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. A /\ E. x x e. B /\ E. y B R y ) ) )

Proof

Step	Hyp	Ref	Expression
1		eldmres	|- ( B e. V -> ( B e. dom ( R |` A ) <-> ( B e. A /\ E. y B R y ) ) )
2		n0	|- ( B =/= (/) <-> E. x x e. B )
3	2	a1i	|- ( B e. V -> ( B =/= (/) <-> E. x x e. B ) )
4	1 3	anbi12d	|- ( B e. V -> ( ( B e. dom ( R |` A ) /\ B =/= (/) ) <-> ( ( B e. A /\ E. y B R y ) /\ E. x x e. B ) ) )
5		dmxrncnvepres	|- dom ( R |X. ( `' _E |` A ) ) = ( dom ( R |` A ) \ { (/) } )
6	5	eleq2i	|- ( B e. dom ( R |X. ( `' _E |` A ) ) <-> B e. ( dom ( R |` A ) \ { (/) } ) )
7		eldifsn	|- ( B e. ( dom ( R |` A ) \ { (/) } ) <-> ( B e. dom ( R |` A ) /\ B =/= (/) ) )
8	6 7	bitri	|- ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. dom ( R |` A ) /\ B =/= (/) ) )
9		3anan32	|- ( ( B e. A /\ E. x x e. B /\ E. y B R y ) <-> ( ( B e. A /\ E. y B R y ) /\ E. x x e. B ) )
10	4 8 9	3bitr4g	|- ( B e. V -> ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. A /\ E. x x e. B /\ E. y B R y ) ) )