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

Theorem psseq2 3577
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 2726 . . 3  |-  ( A  =  B  ->  ( C  =/=  A  <->  C  =/=  B ) )
31, 2anbi12d 710 . 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 369    = wceq 1383    =/= wne 2638    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 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-ne 2640  df-in 3468  df-ss 3475  df-pss 3477
This theorem is referenced by:  psseq2i  3579  psseq2d  3582  psssstr  3595  brrpssg  6567  sorpssint  6575  php  7703  php2  7704  pssnn  7740  isfin4  8680  fin2i2  8701  elnp  9368  elnpi  9369  ltprord  9411  pgpfac1lem1  16999  pgpfac1lem5  17004  lbsextlem4  17681  alexsubALTlem4  20423  spansncv  26443  cvbr  27073  cvcon3  27075  cvnbtwn  27077  cvbr4i  27158  dfon2lem6  29195  dfon2lem7  29196  dfon2lem8  29197  dfon2  29199  lcvbr  34486  lcvnbtwn  34490  lsatcv0  34496  lsat0cv  34498  islshpcv  34518  mapdcv  37127
  Copyright terms: Public domain W3C validator