Metamath Proof Explorer

Theorem elecxrn

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

Ref Expression
Assertion elecxrn 
|- ( A e. V -> ( B e. [ A ] ( R |X. S ) <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) ) )

Proof

Step Hyp Ref Expression
1 xrnrel 
 |-  Rel ( R |X. S )
2 relelec 
 |-  ( Rel ( R |X. S ) -> ( B e. [ A ] ( R |X. S ) <-> A ( R |X. S ) B ) )
3 1 2 ax-mp 
 |-  ( B e. [ A ] ( R |X. S ) <-> A ( R |X. S ) B )
4 brxrn2 
 |-  ( A e. V -> ( A ( R |X. S ) B <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) ) )
5 3 4 bitrid 
 |-  ( A e. V -> ( B e. [ A ] ( R |X. S ) <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) ) )