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

Theorem psseq1 3596
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 3530 . . 3  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
2 neeq1 2748 . . 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 3497 . 2  |-  ( A 
C.  C  <->  ( A  C_  C  /\  A  =/= 
C ) )
5 df-pss 3497 . 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 1379    =/= wne 2662    C_ wss 3481    C. wpss 3482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ne 2664  df-in 3488  df-ss 3495  df-pss 3497
This theorem is referenced by:  psseq1i  3598  psseq1d  3601  psstr  3613  sspsstr  3614  brrpssg  6577  sorpssuni  6584  pssnn  7750  marypha1lem  7905  infeq5i  8065  infpss  8609  fin4i  8690  isfin2-2  8711  zornn0g  8897  ttukeylem7  8907  elnp  9377  elnpi  9378  ltprord  9420  pgpfac1lem1  16997  pgpfac1lem5  17002  pgpfac1  17003  pgpfaclem2  17005  pgpfac  17007  islbs3  17672  alexsubALTlem4  20418  wilthlem2  23209  spansncv  26394  cvbr  27024  cvcon3  27026  cvnbtwn  27028  dfon2lem3  29144  dfon2lem4  29145  dfon2lem5  29146  dfon2lem6  29147  dfon2lem7  29148  dfon2lem8  29149  dfon2  29151  lcvbr  34219  lcvnbtwn  34223  mapdcv  36858
  Copyright terms: Public domain W3C validator