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

Theorem psseq2 3264
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 3200 . . 3  |-  ( A  =  B  ->  ( C  C_  A  <->  C  C_  B
) )
2 neeq2 2455 . . 3  |-  ( A  =  B  ->  ( C  =/=  A  <->  C  =/=  B ) )
31, 2anbi12d 691 . 2  |-  ( A  =  B  ->  (
( C  C_  A  /\  C  =/=  A
)  <->  ( C  C_  B  /\  C  =/=  B
) ) )
4 df-pss 3168 . 2  |-  ( C 
C.  A  <->  ( C  C_  A  /\  C  =/= 
A ) )
5 df-pss 3168 . 2  |-  ( C 
C.  B  <->  ( C  C_  B  /\  C  =/= 
B ) )
63, 4, 53bitr4g 279 1  |-  ( A  =  B  ->  ( C  C.  A  <->  C  C.  B ) )
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:  psseq2i  3266  psseq2d  3269  psssstr  3282  brrpssg  6279  sorpssint  6287  php  7045  php2  7046  pssnn  7081  isfin4  7923  fin2i2  7944  elnp  8611  elnpi  8612  ltprord  8654  pgpfac1lem1  15309  pgpfac1lem5  15314  lbsextlem4  15914  alexsubALTlem4  17744  spansncv  22232  cvbr  22862  cvcon3  22864  cvnbtwn  22866  cvbr4i  22947  dfon2lem6  24144  dfon2lem7  24145  dfon2lem8  24146  dfon2  24148  lcvbr  29211  lcvnbtwn  29215  lsatcv0  29221  lsat0cv  29223  islshpcv  29243  mapdcv  31850
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