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 ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴𝑅 𝐵𝐵𝑅 𝐴 ) )

Proof

Step Hyp Ref Expression
1 exancom ( ∃ 𝑢 ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐵 ) ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐵𝑢 𝑅 𝐴 ) )
2 1 a1i ( ( 𝐴𝑉𝐵𝑊 ) → ( ∃ 𝑢 ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐵 ) ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐵𝑢 𝑅 𝐴 ) ) )
3 brcoss ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴𝑅 𝐵 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐴𝑢 𝑅 𝐵 ) ) )
4 brcoss ( ( 𝐵𝑊𝐴𝑉 ) → ( 𝐵𝑅 𝐴 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐵𝑢 𝑅 𝐴 ) ) )
5 4 ancoms ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐵𝑅 𝐴 ↔ ∃ 𝑢 ( 𝑢 𝑅 𝐵𝑢 𝑅 𝐴 ) ) )
6 2 3 5 3bitr4d ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴𝑅 𝐵𝐵𝑅 𝐴 ) )