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

Definition df-pss 3143
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 20758). Note that  -.  A  C.  A (proved in pssirr 3251). Contrast this relationship with the relationship  A 
C_  B (as defined in df-ss 3141). Other possible definitions are given by dfpss2 3236 and dfpss3 3237. (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 3128 . 2  wff  A  C.  B
41, 2wss 3127 . . 3  wff  A  C_  B
51, 2wne 2421 . . 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  3236  psseq1  3238  psseq2  3239  pssss  3246  pssne  3247  nssinpss  3376  0pss  3467  pssdif  3491  difsnpss  3732  ordelpss  4392  fisseneq  7042  ominf  7043  f1finf1o  7054  fofinf1o  7105  inf3lem2  7298  inf3lem4  7300  infeq5  7306  fin23lem31  7937  isf32lem6  7952  canth4  8237  ipolt  14224  slwpss  14885  lssnle  14945  pgpfaclem2  15279  lspsncv0  15861  islbs3  15870  lbsextlem4  15876  lidlnz  15942  filssufilg  17568  alexsubALTlem4  17706  ppiltx  20377  ex-pss  20758  ch0pss  21984  nepss  23444  dfon2  23517  trelpss  27028  lshpnelb  28341  lshpcmp  28345  lsatssn0  28359  lcvbr3  28380  lsatcv0  28388  lsat0cv  28390  lcvexchlem1  28391  islshpcv  28410  lkrpssN  28520  lkreqN  28527  osumcllem11N  29322  pexmidlem8N  29333  dochsordN  30731  dochsat  30740  dochshpncl  30741  dochexmidlem8  30824  mapdsord  31012
  Copyright terms: Public domain W3C validator