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 A V B W A S -1 = B S -1 A = B

Proof

Step Hyp Ref Expression
1 brssr A V x S A x A
2 brssr B W x S B x B
3 1 2 bi2bian9 A V B W x S A x S B x A x B
4 3 albidv A V B W x x S A x S B x x A x B
5 relssr Rel S
6 releccnveq Rel S Rel S A S -1 = B S -1 x x S A x S B
7 5 5 6 mp2an A S -1 = B S -1 x x S A x S B
8 ssext A = B x x A x B
9 4 7 8 3bitr4g A V B W A S -1 = B S -1 A = B