Metamath Proof Explorer

Theorem psseq1

Description: Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996)

Ref Expression
Assertion psseq1 
|- ( A = B -> ( A C. C <-> B C. C ) )

Proof

Step Hyp Ref Expression
1 sseq1 
 |-  ( A = B -> ( A C_ C <-> B C_ C ) )
2 neeq1 
 |-  ( A = B -> ( A =/= C <-> B =/= C ) )
3 1 2 anbi12d 
 |-  ( A = B -> ( ( A C_ C /\ A =/= C ) <-> ( B C_ C /\ B =/= C ) ) )
4 df-pss 
 |-  ( A C. C <-> ( A C_ C /\ A =/= C ) )
5 df-pss 
 |-  ( B C. C <-> ( B C_ C /\ B =/= C ) )
6 3 4 5 3bitr4g 
 |-  ( A = B -> ( A C. C <-> B C. C ) )