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

Definition df-pss 3168
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 20815). Note that  -.  A  C.  A (proved in pssirr 3276). Contrast this relationship with the relationship  A 
C_  B (as defined in df-ss 3166). Other possible definitions are given by dfpss2 3261 and dfpss3 3262. (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 3153 . 2  wff  A  C.  B
41, 2wss 3152 . . 3  wff  A  C_  B
51, 2wne 2446 . . 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  3261  psseq1  3263  psseq2  3264  pssss  3271  pssne  3272  nssinpss  3401  0pss  3492  pssdif  3516  difsnpss  3758  ordelpss  4420  fisseneq  7074  ominf  7075  f1finf1o  7086  fofinf1o  7137  inf3lem2  7330  inf3lem4  7332  infeq5  7338  fin23lem31  7969  isf32lem6  7984  canth4  8269  ipolt  14262  slwpss  14923  lssnle  14983  pgpfaclem2  15317  lspsncv0  15899  islbs3  15908  lbsextlem4  15914  lidlnz  15980  filssufilg  17606  alexsubALTlem4  17744  ppiltx  20415  ex-pss  20815  ch0pss  22024  nepss  24072  dfon2  24148  trelpss  27660  lshpnelb  29174  lshpcmp  29178  lsatssn0  29192  lcvbr3  29213  lsatcv0  29221  lsat0cv  29223  lcvexchlem1  29224  islshpcv  29243  lkrpssN  29353  lkreqN  29360  osumcllem11N  30155  pexmidlem8N  30166  dochsordN  31564  dochsat  31573  dochshpncl  31574  dochexmidlem8  31657  mapdsord  31845
  Copyright terms: Public domain W3C validator