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

Definition df-pss 3110
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 20723). Note that  -.  A  C.  A (proved in pssirr 3218). Contrast this relationship with the relationship  A 
C_  B (as defined in df-ss 3108). Other possible definitions are given by dfpss2 3203 and dfpss3 3204. (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 3095 . 2  wff  A  C.  B
41, 2wss 3094 . . 3  wff  A  C_  B
51, 2wne 2419 . . 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  3203  psseq1  3205  psseq2  3206  pssss  3213  pssne  3214  nssinpss  3343  0pss  3434  pssdif  3458  difsnpss  3699  ordelpss  4357  fisseneq  7007  ominf  7008  f1finf1o  7019  fofinf1o  7070  inf3lem2  7263  inf3lem4  7265  infeq5  7271  fin23lem31  7902  isf32lem6  7917  canth4  8202  ipolt  14189  slwpss  14850  lssnle  14910  pgpfaclem2  15244  lspsncv0  15826  islbs3  15835  lbsextlem4  15841  lidlnz  15907  filssufilg  17533  alexsubALTlem4  17671  ppiltx  20342  ex-pss  20723  ch0pss  21949  nepss  23409  dfon2  23482  trelpss  26993  lshpnelb  28304  lshpcmp  28308  lsatssn0  28322  lcvbr3  28343  lsatcv0  28351  lsat0cv  28353  lcvexchlem1  28354  islshpcv  28373  lkrpssN  28483  lkreqN  28490  osumcllem11N  29285  pexmidlem8N  29296  dochsordN  30694  dochsat  30703  dochshpncl  30704  dochexmidlem8  30787  mapdsord  30975
  Copyright terms: Public domain W3C validator