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

Definition df-pss 3091
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 20628). Note that  -.  A  C.  A (proved in pssirr 3196). Contrast this relationship with the relationship  A 
C_  B (as defined in df-ss 3089). Other possible definitions are given by dfpss2 3182 and dfpss3 3183. (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 3079 . 2  wff  A  C.  B
41, 2wss 3078 . . 3  wff  A  C_  B
51, 2wne 2412 . . 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  3182  psseq1  3184  psseq2  3185  pssss  3192  pssne  3193  nssinpss  3308  0pss  3399  pssdif  3423  ordelpss  4313  fisseneq  6959  ominf  6960  f1finf1o  6971  fofinf1o  7022  inf3lem2  7214  inf3lem4  7216  infeq5  7222  fin23lem31  7853  isf32lem6  7868  canth4  8149  ipolt  14106  slwpss  14758  lssnle  14818  pgpfaclem2  15152  lspsncv0  15733  islbs3  15742  lbsextlem4  15746  lidlnz  15812  filssufilg  17438  alexsubALTlem4  17576  ppiltx  20247  ex-pss  20628  ch0pss  21854  nepss  23243  dfon2  23316  trelpss  26827  lshpnelb  27975  lshpcmp  27979  lsatssn0  27993  lcvbr3  28014  lsatcv0  28022  lsat0cv  28024  lcvexchlem1  28025  islshpcv  28044  lkrpssN  28154  lkreqN  28161  osumcllem11N  28956  pexmidlem8N  28967  dochsordN  30365  dochsat  30374  dochshpncl  30375  dochexmidlem8  30458  mapdsord  30646
  Copyright terms: Public domain W3C validator