Metamath Proof Explorer

Theorem seeq1

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

Ref Expression
Assertion seeq1 
|- ( R = S -> ( R Se A <-> S Se A ) )

Proof

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