Metamath Proof Explorer

Theorem brcosscnvcoss

Description: For sets, the A and B cosets by R binary relation and the B and A cosets by R binary relation are the same. (Contributed by Peter Mazsa, 27-Dec-2018)

Ref Expression
Assertion brcosscnvcoss ⊢ A ∈ V ∧ B ∈ W → A ≀ R B ↔ B ≀ R A

Proof

Step Hyp Ref Expression
1 exancom ⊢ ∃ u u R A ∧ u R B ↔ ∃ u u R B ∧ u R A
2 1 a1i ⊢ A ∈ V ∧ B ∈ W → ∃ u u R A ∧ u R B ↔ ∃ u u R B ∧ u R A
3 brcoss ⊢ A ∈ V ∧ B ∈ W → A ≀ R B ↔ ∃ u u R A ∧ u R B
4 brcoss ⊢ B ∈ W ∧ A ∈ V → B ≀ R A ↔ ∃ u u R B ∧ u R A
5 4 ancoms ⊢ A ∈ V ∧ B ∈ W → B ≀ R A ↔ ∃ u u R B ∧ u R A
6 2 3 5 3bitr4d ⊢ A ∈ V ∧ B ∈ W → A ≀ R B ↔ B ≀ R A