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 = B -> ( R Se A <-> R Se B ) )

Proof

Step Hyp Ref Expression
1 eqimss2 
 |-  ( A = B -> B C_ A )
2 sess2 
 |-  ( B C_ A -> ( R Se A -> R Se B ) )
3 1 2 syl 
 |-  ( A = B -> ( R Se A -> R Se B ) )
4 eqimss 
 |-  ( A = B -> A C_ B )
5 sess2 
 |-  ( A C_ B -> ( R Se B -> R Se A ) )
6 4 5 syl 
 |-  ( A = B -> ( R Se B -> R Se A ) )
7 3 6 impbid 
 |-  ( A = B -> ( R Se A <-> R Se B ) )