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 V A R S = y z | A R y A S z

Proof

Step Hyp Ref Expression
1 elecxrn A V x A R S y 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 y z x = y z A R y A S z y z x = y z A R y A S z
4 1 3 bitrdi A V x A R S y z x = y z A R y A S z
5 elopab x y z | A R y A S z y z x = y z A R y A S z
6 4 5 bitr4di A V x A R S x y z | A R y A S z
7 6 eqrdv A V A R S = y z | A R y A S z