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\in V\to \left(B\in \left[A\right]R⋉S\leftrightarrow \exists x\exists y\left(B=⟨x,y⟩\wedge ARx\wedge ASy\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrnrel	$$⊢\mathrm{Rel}R⋉S$$
2		relelec	$$⊢\mathrm{Rel}R⋉S\to \left(B\in \left[A\right]R⋉S\leftrightarrow AR⋉SB\right)$$
3	1 2	ax-mp	$$⊢B\in \left[A\right]R⋉S\leftrightarrow AR⋉SB$$
4		brxrn2	$$⊢A\in V\to \left(AR⋉SB\leftrightarrow \exists x\exists y\left(B=⟨x,y⟩\wedge ARx\wedge ASy\right)\right)$$
5	3 4	bitrid	$$⊢A\in V\to \left(B\in \left[A\right]R⋉S\leftrightarrow \exists x\exists y\left(B=⟨x,y⟩\wedge ARx\wedge ASy\right)\right)$$