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

Theorem psseq2 3578
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 3511 . . 3  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
2 neeq2 2737 . . 3  |-  ( A  =  B  ->  ( C  =/=  A  <->  C  =/=  B ) )
31, 2anbi12d 708 . 2  |-  ( A  =  B  ->  (
( C  C_  A  /\  C  =/=  A
)  <->  ( C  C_  B  /\  C  =/=  B
) ) )
4 df-pss 3477 . 2  |-  ( C 
C.  A  <->  ( C  C_  A  /\  C  =/= 
A ) )
5 df-pss 3477 . 2  |-  ( C 
C.  B  <->  ( C  C_  B  /\  C  =/= 
B ) )
63, 4, 53bitr4g 288 1  |-  ( A  =  B  ->  ( C  C.  A  <->  C  C.  B
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1398    =/= wne 2649    C_ wss 3461    C. wpss 3462
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-ne 2651  df-in 3468  df-ss 3475  df-pss 3477
This theorem is referenced by:  psseq2i  3580  psseq2d  3583  psssstr  3596  brrpssg  6555  sorpssint  6563  php  7694  php2  7695  pssnn  7731  isfin4  8668  fin2i2  8689  elnp  9354  elnpi  9355  ltprord  9397  pgpfac1lem1  17320  pgpfac1lem5  17325  lbsextlem4  18002  alexsubALTlem4  20716  spansncv  26769  cvbr  27399  cvcon3  27401  cvnbtwn  27403  cvbr4i  27484  dfon2lem6  29460  dfon2lem7  29461  dfon2lem8  29462  dfon2  29464  lcvbr  35143  lcvnbtwn  35147  lsatcv0  35153  lsat0cv  35155  islshpcv  35175  mapdcv  37784
  Copyright terms: Public domain W3C validator