This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V → B ∈ A R ⋉ S ↔ ∃ x ∃ y B = x y ∧ A R x ∧ A S y

Proof

Step Hyp Ref Expression
1 xrnrel ⊢ Rel ⁡ R ⋉ S
2 relelec ⊢ Rel ⁡ R ⋉ S → B ∈ A R ⋉ S ↔ A R ⋉ S B
3 1 2 ax-mp ⊢ B ∈ A R ⋉ S ↔ A R ⋉ S B
4 brxrn2 ⊢ A ∈ V → A R ⋉ S B ↔ ∃ x ∃ y B = x y ∧ A R x ∧ A S y
5 3 4 bitrid ⊢ A ∈ V → B ∈ A R ⋉ S ↔ ∃ x ∃ y B = x y ∧ A R x ∧ A S y