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

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

Proof of Theorem psseq2
StepHypRef Expression
1 sseq2 3362 . . 3  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
2 neeq2 2607 . . 3  |-  ( A  =  B  ->  ( C  =/=  A  <->  C  =/=  B ) )
31, 2anbi12d 692 . 2  |-  ( A  =  B  ->  (
( C  C_  A  /\  C  =/=  A
)  <->  ( C  C_  B  /\  C  =/=  B
) ) )
4 df-pss 3328 . 2  |-  ( C 
C.  A  <->  ( C  C_  A  /\  C  =/= 
A ) )
5 df-pss 3328 . 2  |-  ( C 
C.  B  <->  ( C  C_  B  /\  C  =/= 
B ) )
63, 4, 53bitr4g 280 1  |-  ( A  =  B  ->  ( C  C.  A  <->  C  C.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652    =/= wne 2598    C_ wss 3312    C. wpss 3313
This theorem is referenced by:  psseq2i  3429  psseq2d  3432  psssstr  3445  brrpssg  6516  sorpssint  6524  php  7283  php2  7284  pssnn  7319  isfin4  8167  fin2i2  8188  elnp  8854  elnpi  8855  ltprord  8897  pgpfac1lem1  15622  pgpfac1lem5  15627  lbsextlem4  16223  alexsubALTlem4  18071  spansncv  23145  cvbr  23775  cvcon3  23777  cvnbtwn  23779  cvbr4i  23860  dfon2lem6  25403  dfon2lem7  25404  dfon2lem8  25405  dfon2  25407  lcvbr  29720  lcvnbtwn  29724  lsatcv0  29730  lsat0cv  29732  islshpcv  29752  mapdcv  32359
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-ne 2600  df-in 3319  df-ss 3326  df-pss 3328
  Copyright terms: Public domain W3C validator