Theorem ecelqsdmb

Description: R -coset of B in a quotient set, biconditional version. (Contributed by Peter Mazsa, 17-Apr-2019) (Revised by Peter Mazsa, 22-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ecelqsdm	|- ( ( dom R = A /\ [ B ] R e. ( A /. R ) ) -> B e. A )
2	1	ex	|- ( dom R = A -> ( [ B ] R e. ( A /. R ) -> B e. A ) )
3	2	adantl	|- ( ( ( R |` A ) e. V /\ dom R = A ) -> ( [ B ] R e. ( A /. R ) -> B e. A ) )
4		ecelqs	|- ( ( ( R |` A ) e. V /\ B e. A ) -> [ B ] R e. ( A /. R ) )
5	4	ex	|- ( ( R |` A ) e. V -> ( B e. A -> [ B ] R e. ( A /. R ) ) )
6	5	adantr	|- ( ( ( R |` A ) e. V /\ dom R = A ) -> ( B e. A -> [ B ] R e. ( A /. R ) ) )
7	3 6	impbid	|- ( ( ( R |` A ) e. V /\ dom R = A ) -> ( [ B ] R e. ( A /. R ) <-> B e. A ) )