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

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

Proof of Theorem psseq1
StepHypRef Expression
1 sseq1 3377 . . 3  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
2 neeq1 2616 . . 3  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
31, 2anbi12d 710 . 2  |-  ( A  =  B  ->  (
( A  C_  C  /\  A  =/=  C
)  <->  ( B  C_  C  /\  B  =/=  C
) ) )
4 df-pss 3344 . 2  |-  ( A 
C.  C  <->  ( A  C_  C  /\  A  =/= 
C ) )
5 df-pss 3344 . 2  |-  ( B 
C.  C  <->  ( B  C_  C  /\  B  =/= 
C ) )
63, 4, 53bitr4g 288 1  |-  ( A  =  B  ->  ( A  C.  C  <->  B  C.  C
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    =/= wne 2606    C_ wss 3328    C. wpss 3329
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-ne 2608  df-in 3335  df-ss 3342  df-pss 3344
This theorem is referenced by:  psseq1i  3445  psseq1d  3448  psstr  3460  sspsstr  3461  brrpssg  6362  sorpssuni  6369  pssnn  7531  marypha1lem  7683  infeq5i  7842  infpss  8386  fin4i  8467  isfin2-2  8488  zornn0g  8674  ttukeylem7  8684  elnp  9156  elnpi  9157  ltprord  9199  pgpfac1lem1  16575  pgpfac1lem5  16580  pgpfac1  16581  pgpfaclem2  16583  pgpfac  16585  islbs3  17236  alexsubALTlem4  19622  wilthlem2  22407  spansncv  25056  cvbr  25686  cvcon3  25688  cvnbtwn  25690  dfon2lem3  27598  dfon2lem4  27599  dfon2lem5  27600  dfon2lem6  27601  dfon2lem7  27602  dfon2lem8  27603  dfon2  27605  lcvbr  32666  lcvnbtwn  32670  mapdcv  35305
  Copyright terms: Public domain W3C validator