# Metamath Proof Explorer

## Theorem extssr

Description: Property of subset relation, see also extid , extep and the comment of df-ssr . (Contributed by Peter Mazsa, 10-Jul-2019)

Ref Expression
Assertion extssr ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left[{A}\right]{\mathrm{S}}^{-1}=\left[{B}\right]{\mathrm{S}}^{-1}↔{A}={B}\right)$

### Proof

Step Hyp Ref Expression
1 brssr ${⊢}{A}\in {V}\to \left({x}\mathrm{S}{A}↔{x}\subseteq {A}\right)$
2 brssr ${⊢}{B}\in {W}\to \left({x}\mathrm{S}{B}↔{x}\subseteq {B}\right)$
3 1 2 bi2bian9 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left({x}\mathrm{S}{A}↔{x}\mathrm{S}{B}\right)↔\left({x}\subseteq {A}↔{x}\subseteq {B}\right)\right)$
4 3 albidv ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{S}{A}↔{x}\mathrm{S}{B}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {A}↔{x}\subseteq {B}\right)\right)$
5 relssr ${⊢}\mathrm{Rel}\mathrm{S}$
6 releccnveq ${⊢}\left(\mathrm{Rel}\mathrm{S}\wedge \mathrm{Rel}\mathrm{S}\right)\to \left(\left[{A}\right]{\mathrm{S}}^{-1}=\left[{B}\right]{\mathrm{S}}^{-1}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{S}{A}↔{x}\mathrm{S}{B}\right)\right)$
7 5 5 6 mp2an ${⊢}\left[{A}\right]{\mathrm{S}}^{-1}=\left[{B}\right]{\mathrm{S}}^{-1}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{S}{A}↔{x}\mathrm{S}{B}\right)$
8 ssext ${⊢}{A}={B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {A}↔{x}\subseteq {B}\right)$
9 4 7 8 3bitr4g ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left[{A}\right]{\mathrm{S}}^{-1}=\left[{B}\right]{\mathrm{S}}^{-1}↔{A}={B}\right)$