Metamath Proof Explorer


Theorem seeq2

Description: Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion seeq2 A=BRSeARSeB

Proof

Step Hyp Ref Expression
1 eqimss2 A=BBA
2 sess2 BARSeARSeB
3 1 2 syl A=BRSeARSeB
4 eqimss A=BAB
5 sess2 ABRSeBRSeA
6 4 5 syl A=BRSeBRSeA
7 3 6 impbid A=BRSeARSeB