Metamath Proof Explorer

Theorem br1cnvxrn2

Description: The converse of a binary relation over a range Cartesian product. (Contributed by Peter Mazsa, 11-Jul-2021)

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

Proof

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