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

Definition df-pss 3336
Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example,  { 1 ,  2 }  C.  {
1 ,  2 ,  3 } (ex-pss 21736). Note that  -.  A  C.  A (proved in pssirr 3447). Contrast this relationship with the relationship  A 
C_  B (as defined in df-ss 3334). Other possible definitions are given by dfpss2 3432 and dfpss3 3433. (Contributed by NM, 7-Feb-1996.)
Assertion
Ref Expression
df-pss  |-  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )

Detailed syntax breakdown of Definition df-pss
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2wpss 3321 . 2  wff  A  C.  B
41, 2wss 3320 . . 3  wff  A  C_  B
51, 2wne 2599 . . 3  wff  A  =/= 
B
64, 5wa 359 . 2  wff  ( A 
C_  B  /\  A  =/=  B )
73, 6wb 177 1  wff  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
Colors of variables: wff set class
This definition is referenced by:  dfpss2  3432  psseq1  3434  psseq2  3435  pssss  3442  pssne  3443  nssinpss  3573  0pss  3665  pssdif  3690  difsnpss  3941  ordelpss  4609  fisseneq  7320  ominf  7321  f1finf1o  7335  fofinf1o  7387  inf3lem2  7584  inf3lem4  7586  infeq5  7592  fin23lem31  8223  isf32lem6  8238  ipolt  14585  lssnle  15306  pgpfaclem2  15640  lspsncv0  16218  islbs3  16227  lbsextlem4  16233  lidlnz  16299  filssufilg  17943  alexsubALTlem4  18081  ppiltx  20960  ex-pss  21736  ch0pss  22947  nepss  25175  dfon2  25419  trelpss  27636  lshpnelb  29782  lshpcmp  29786  lsatssn0  29800  lcvbr3  29821  lsatcv0  29829  lsat0cv  29831  lcvexchlem1  29832  islshpcv  29851  lkrpssN  29961  lkreqN  29968  osumcllem11N  30763  pexmidlem8N  30774  dochsordN  32172  dochsat  32181  dochshpncl  32182  dochexmidlem8  32265  mapdsord  32453
  Copyright terms: Public domain W3C validator