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

Definition df-pss 3328
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 21724). Note that  -.  A  C.  A (proved in pssirr 3439). Contrast this relationship with the relationship  A 
C_  B (as defined in df-ss 3326). Other possible definitions are given by dfpss2 3424 and dfpss3 3425. (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 3313 . 2  wff  A  C.  B
41, 2wss 3312 . . 3  wff  A  C_  B
51, 2wne 2598 . . 3  wff  A  =/= 
B
64, 5wa 359 . 2  wff  ( A 
C_  B  /\  A  =/=  B )
73, 6wb 177 1  wff  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
Colors of variables: wff set class
This definition is referenced by:  dfpss2  3424  psseq1  3426  psseq2  3427  pssss  3434  pssne  3435  nssinpss  3565  0pss  3657  pssdif  3682  difsnpss  3933  ordelpss  4601  fisseneq  7311  ominf  7312  f1finf1o  7326  fofinf1o  7378  inf3lem2  7573  inf3lem4  7575  infeq5  7581  fin23lem31  8212  isf32lem6  8227  ipolt  14573  lssnle  15294  pgpfaclem2  15628  lspsncv0  16206  islbs3  16215  lbsextlem4  16221  lidlnz  16287  filssufilg  17931  alexsubALTlem4  18069  ppiltx  20948  ex-pss  21724  ch0pss  22935  nepss  25163  dfon2  25403  trelpss  27574  lshpnelb  29621  lshpcmp  29625  lsatssn0  29639  lcvbr3  29660  lsatcv0  29668  lsat0cv  29670  lcvexchlem1  29671  islshpcv  29690  lkrpssN  29800  lkreqN  29807  osumcllem11N  30602  pexmidlem8N  30613  dochsordN  32011  dochsat  32020  dochshpncl  32021  dochexmidlem8  32104  mapdsord  32292
  Copyright terms: Public domain W3C validator