MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  psseq2 Unicode version

Theorem psseq2 3378
Description: Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)
Assertion
Ref Expression
psseq2  |-  ( A  =  B  ->  ( C  C.  A  <->  C  C.  B ) )

Proof of Theorem psseq2
StepHypRef Expression
1 sseq2 3313 . . 3  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
2 neeq2 2559 . . 3  |-  ( A  =  B  ->  ( C  =/=  A  <->  C  =/=  B ) )
31, 2anbi12d 692 . 2  |-  ( A  =  B  ->  (
( C  C_  A  /\  C  =/=  A
)  <->  ( C  C_  B  /\  C  =/=  B
) ) )
4 df-pss 3279 . 2  |-  ( C 
C.  A  <->  ( C  C_  A  /\  C  =/= 
A ) )
5 df-pss 3279 . 2  |-  ( C 
C.  B  <->  ( C  C_  B  /\  C  =/= 
B ) )
63, 4, 53bitr4g 280 1  |-  ( A  =  B  ->  ( C  C.  A  <->  C  C.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    =/= wne 2550    C_ wss 3263    C. wpss 3264
This theorem is referenced by:  psseq2i  3380  psseq2d  3383  psssstr  3396  brrpssg  6460  sorpssint  6468  php  7227  php2  7228  pssnn  7263  isfin4  8110  fin2i2  8131  elnp  8797  elnpi  8798  ltprord  8840  pgpfac1lem1  15559  pgpfac1lem5  15564  lbsextlem4  16160  alexsubALTlem4  18002  spansncv  23003  cvbr  23633  cvcon3  23635  cvnbtwn  23637  cvbr4i  23718  dfon2lem6  25168  dfon2lem7  25169  dfon2lem8  25170  dfon2  25172  lcvbr  29136  lcvnbtwn  29140  lsatcv0  29146  lsat0cv  29148  islshpcv  29168  mapdcv  31775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-ne 2552  df-in 3270  df-ss 3277  df-pss 3279
  Copyright terms: Public domain W3C validator