Theorem eceldmqsxrncnvepres

Description: An ( R |X. ( ' E | A ) ) -coset in its domain quotient. (Contributed by Peter Mazsa, 23-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		xrncnvepresex	|- ( ( A e. V /\ R e. X ) -> ( R |X. ( `' _E |` A ) ) e. _V )
2		eceldmqs	|- ( ( R |X. ( `' _E |` A ) ) e. _V -> ( [ B ] ( R |X. ( `' _E |` A ) ) e. ( dom ( R |X. ( `' _E |` A ) ) /. ( R |X. ( `' _E |` A ) ) ) <-> B e. dom ( R |X. ( `' _E |` A ) ) ) )
3	1 2	syl	|- ( ( A e. V /\ R e. X ) -> ( [ B ] ( R |X. ( `' _E |` A ) ) e. ( dom ( R |X. ( `' _E |` A ) ) /. ( R |X. ( `' _E |` A ) ) ) <-> B e. dom ( R |X. ( `' _E |` A ) ) ) )
4	3	3adant2	|- ( ( A e. V /\ B e. W /\ R e. X ) -> ( [ B ] ( R |X. ( `' _E |` A ) ) e. ( dom ( R |X. ( `' _E |` A ) ) /. ( R |X. ( `' _E |` A ) ) ) <-> B e. dom ( R |X. ( `' _E |` A ) ) ) )
5		eldmxrncnvepres	|- ( B e. W -> ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. A /\ B =/= (/) /\ [ B ] R =/= (/) ) ) )
6	5	3ad2ant2	|- ( ( A e. V /\ B e. W /\ R e. X ) -> ( B e. dom ( R |X. ( `' _E |` A ) ) <-> ( B e. A /\ B =/= (/) /\ [ B ] R =/= (/) ) ) )
7	4 6	bitrd	|- ( ( A e. V /\ B e. W /\ R e. X ) -> ( [ B ] ( R |X. ( `' _E |` A ) ) e. ( dom ( R |X. ( `' _E |` A ) ) /. ( R |X. ( `' _E |` A ) ) ) <-> ( B e. A /\ B =/= (/) /\ [ B ] R =/= (/) ) ) )