Metamath Proof Explorer

Theorem ecxrn

Description: The ( R |X. S ) -coset of A . (Contributed by Peter Mazsa, 18-Apr-2020) (Revised by Peter Mazsa, 21-Sep-2021)

Ref Expression
Assertion ecxrn 
|- ( A e. V -> [ A ] ( R |X. S ) = { <. y , z >. | ( A R y /\ A S z ) } )

Proof

Step Hyp Ref Expression
1 elecxrn 
 |-  ( A e. V -> ( x e. [ A ] ( R |X. S ) <-> E. y E. z ( x = <. y , z >. /\ A R y /\ A S z ) ) )
2 3anass 
 |-  ( ( x = <. y , z >. /\ A R y /\ A S z ) <-> ( x = <. y , z >. /\ ( A R y /\ A S z ) ) )
3 2 2exbii 
 |-  ( E. y E. z ( x = <. y , z >. /\ A R y /\ A S z ) <-> E. y E. z ( x = <. y , z >. /\ ( A R y /\ A S z ) ) )
4 1 3 bitrdi 
 |-  ( A e. V -> ( x e. [ A ] ( R |X. S ) <-> E. y E. z ( x = <. y , z >. /\ ( A R y /\ A S z ) ) ) )
5 elopab 
 |-  ( x e. { <. y , z >. | ( A R y /\ A S z ) } <-> E. y E. z ( x = <. y , z >. /\ ( A R y /\ A S z ) ) )
6 4 5 bitr4di 
 |-  ( A e. V -> ( x e. [ A ] ( R |X. S ) <-> x e. { <. y , z >. | ( A R y /\ A S z ) } ) )
7 6 eqrdv 
 |-  ( A e. V -> [ A ] ( R |X. S ) = { <. y , z >. | ( A R y /\ A S z ) } )