This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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