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 ) ) ) |
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 | syl5bb | |- ( A e. V -> ( B e. [ A ] ( R |X. S ) <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) ) ) |