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

Definition df-pss 3181
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 20831). Note that  -.  A  C.  A (proved in pssirr 3289). Contrast this relationship with the relationship  A 
C_  B (as defined in df-ss 3179). Other possible definitions are given by dfpss2 3274 and dfpss3 3275. (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 3166 . 2  wff  A  C.  B
41, 2wss 3165 . . 3  wff  A  C_  B
51, 2wne 2459 . . 3  wff  A  =/= 
B
64, 5wa 358 . 2  wff  ( A 
C_  B  /\  A  =/=  B )
73, 6wb 176 1  wff  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
Colors of variables: wff set class
This definition is referenced by:  dfpss2  3274  psseq1  3276  psseq2  3277  pssss  3284  pssne  3285  nssinpss  3414  0pss  3505  pssdif  3529  difsnpss  3774  ordelpss  4436  fisseneq  7090  ominf  7091  f1finf1o  7102  fofinf1o  7153  inf3lem2  7346  inf3lem4  7348  infeq5  7354  fin23lem31  7985  isf32lem6  8000  canth4  8285  ipolt  14278  slwpss  14939  lssnle  14999  pgpfaclem2  15333  lspsncv0  15915  islbs3  15924  lbsextlem4  15930  lidlnz  15996  filssufilg  17622  alexsubALTlem4  17760  ppiltx  20431  ex-pss  20831  ch0pss  22040  nepss  24087  dfon2  24219  trelpss  27763  lshpnelb  29796  lshpcmp  29800  lsatssn0  29814  lcvbr3  29835  lsatcv0  29843  lsat0cv  29845  lcvexchlem1  29846  islshpcv  29865  lkrpssN  29975  lkreqN  29982  osumcllem11N  30777  pexmidlem8N  30788  dochsordN  32186  dochsat  32195  dochshpncl  32196  dochexmidlem8  32279  mapdsord  32467
  Copyright terms: Public domain W3C validator