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

Theorem psseq1 3434
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 3369 . . 3  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
2 neeq1 2609 . . 3  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
31, 2anbi12d 692 . 2  |-  ( A  =  B  ->  (
( A  C_  C  /\  A  =/=  C
)  <->  ( B  C_  C  /\  B  =/=  C
) ) )
4 df-pss 3336 . 2  |-  ( A 
C.  C  <->  ( A  C_  C  /\  A  =/= 
C ) )
5 df-pss 3336 . 2  |-  ( B 
C.  C  <->  ( B  C_  C  /\  B  =/= 
C ) )
63, 4, 53bitr4g 280 1  |-  ( A  =  B  ->  ( A  C.  C  <->  B  C.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652    =/= wne 2599    C_ wss 3320    C. wpss 3321
This theorem is referenced by:  psseq1i  3436  psseq1d  3439  psstr  3451  sspsstr  3452  brrpssg  6524  sorpssuni  6531  pssnn  7327  marypha1lem  7438  infeq5i  7591  infpss  8097  fin4i  8178  isfin2-2  8199  zornn0g  8385  ttukeylem7  8395  elnp  8864  elnpi  8865  ltprord  8907  pgpfac1lem1  15632  pgpfac1lem5  15637  pgpfac1  15638  pgpfaclem2  15640  pgpfac  15642  islbs3  16227  alexsubALTlem4  18081  wilthlem2  20852  spansncv  23155  cvbr  23785  cvcon3  23787  cvnbtwn  23789  dfon2lem3  25412  dfon2lem4  25413  dfon2lem5  25414  dfon2lem6  25415  dfon2lem7  25416  dfon2lem8  25417  dfon2  25419  lcvbr  29819  lcvnbtwn  29823  mapdcv  32458
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-ne 2601  df-in 3327  df-ss 3334  df-pss 3336
  Copyright terms: Public domain W3C validator