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

Definition df-pss 3170
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 20791). Note that  -.  A  C.  A (proved in pssirr 3278). Contrast this relationship with the relationship  A 
C_  B (as defined in df-ss 3168). Other possible definitions are given by dfpss2 3263 and dfpss3 3264. (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 3155 . 2  wff  A  C.  B
41, 2wss 3154 . . 3  wff  A  C_  B
51, 2wne 2448 . . 3  wff  A  =/= 
B
64, 5wa 360 . 2  wff  ( A 
C_  B  /\  A  =/=  B )
73, 6wb 178 1  wff  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
Colors of variables: wff set class
This definition is referenced by:  dfpss2  3263  psseq1  3265  psseq2  3266  pssss  3273  pssne  3274  nssinpss  3403  0pss  3494  pssdif  3518  difsnpss  3760  ordelpss  4420  fisseneq  7070  ominf  7071  f1finf1o  7082  fofinf1o  7133  inf3lem2  7326  inf3lem4  7328  infeq5  7334  fin23lem31  7965  isf32lem6  7980  canth4  8265  ipolt  14257  slwpss  14918  lssnle  14978  pgpfaclem2  15312  lspsncv0  15894  islbs3  15903  lbsextlem4  15909  lidlnz  15975  filssufilg  17601  alexsubALTlem4  17739  ppiltx  20410  ex-pss  20791  ch0pss  22017  nepss  23477  dfon2  23550  trelpss  27060  lshpnelb  28442  lshpcmp  28446  lsatssn0  28460  lcvbr3  28481  lsatcv0  28489  lsat0cv  28491  lcvexchlem1  28492  islshpcv  28511  lkrpssN  28621  lkreqN  28628  osumcllem11N  29423  pexmidlem8N  29434  dochsordN  30832  dochsat  30841  dochshpncl  30842  dochexmidlem8  30925  mapdsord  31113
  Copyright terms: Public domain W3C validator