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

Theorem psseq1 3440
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 3374 . . 3  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
2 neeq1 2614 . . 3  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
31, 2anbi12d 705 . 2  |-  ( A  =  B  ->  (
( A  C_  C  /\  A  =/=  C
)  <->  ( B  C_  C  /\  B  =/=  C
) ) )
4 df-pss 3341 . 2  |-  ( A 
C.  C  <->  ( A  C_  C  /\  A  =/= 
C ) )
5 df-pss 3341 . 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 1364    =/= wne 2604    C_ wss 3325    C. wpss 3326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-ne 2606  df-in 3332  df-ss 3339  df-pss 3341
This theorem is referenced by:  psseq1i  3442  psseq1d  3445  psstr  3457  sspsstr  3458  brrpssg  6361  sorpssuni  6368  pssnn  7527  marypha1lem  7679  infeq5i  7838  infpss  8382  fin4i  8463  isfin2-2  8484  zornn0g  8670  ttukeylem7  8680  elnp  9152  elnpi  9153  ltprord  9195  pgpfac1lem1  16565  pgpfac1lem5  16570  pgpfac1  16571  pgpfaclem2  16573  pgpfac  16575  islbs3  17214  alexsubALTlem4  19581  wilthlem2  22366  spansncv  24991  cvbr  25621  cvcon3  25623  cvnbtwn  25625  dfon2lem3  27527  dfon2lem4  27528  dfon2lem5  27529  dfon2lem6  27530  dfon2lem7  27531  dfon2lem8  27532  dfon2  27534  lcvbr  32388  lcvnbtwn  32392  mapdcv  35027
  Copyright terms: Public domain W3C validator