Metamath Proof Explorer

Theorem elec1cnvxrn2

Description: Elementhood in the converse range Cartesian product coset of A . (Contributed by Peter Mazsa, 11-Jul-2021)

Ref Expression
Assertion elec1cnvxrn2 ⊢ B ∈ V → B ∈ A R ⋉ S -1 ↔ ∃ y ∃ z A = y z ∧ B R y ∧ B S z

Proof

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