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

Theorem psseq1 3263
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 3199 . . 3  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
2 neeq1 2454 . . 3  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
31, 2anbi12d 691 . 2  |-  ( A  =  B  ->  (
( A  C_  C  /\  A  =/=  C
)  <->  ( B  C_  C  /\  B  =/=  C
) ) )
4 df-pss 3168 . 2  |-  ( A 
C.  C  <->  ( A  C_  C  /\  A  =/= 
C ) )
5 df-pss 3168 . 2  |-  ( B 
C.  C  <->  ( B  C_  C  /\  B  =/= 
C ) )
63, 4, 53bitr4g 279 1  |-  ( A  =  B  ->  ( A  C.  C  <->  B  C.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    =/= wne 2446    C_ wss 3152    C. wpss 3153
This theorem is referenced by:  psseq1i  3265  psseq1d  3268  psstr  3280  sspsstr  3281  brrpssg  6279  sorpssuni  6286  pssnn  7081  marypha1lem  7186  infeq5i  7337  infpss  7843  fin4i  7924  isfin2-2  7945  zornn0g  8132  ttukeylem7  8142  elnp  8611  elnpi  8612  ltprord  8654  pgpfac1lem1  15309  pgpfac1lem5  15314  pgpfac1  15315  pgpfaclem2  15317  pgpfac  15319  islbs3  15908  alexsubALTlem4  17744  wilthlem2  20307  spansncv  22232  cvbr  22862  cvcon3  22864  cvnbtwn  22866  dfon2lem3  23552  dfon2lem4  23553  dfon2lem5  23554  dfon2lem6  23555  dfon2lem7  23556  dfon2lem8  23557  dfon2  23559  lcvbr  28584  lcvnbtwn  28588  mapdcv  31223
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ne 2448  df-in 3159  df-ss 3166  df-pss 3168
  Copyright terms: Public domain W3C validator