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

Definition df-pss 3296
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 21689). Note that  -.  A  C.  A (proved in pssirr 3407). Contrast this relationship with the relationship  A 
C_  B (as defined in df-ss 3294). Other possible definitions are given by dfpss2 3392 and dfpss3 3393. (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 3281 . 2  wff  A  C.  B
41, 2wss 3280 . . 3  wff  A  C_  B
51, 2wne 2567 . . 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  3392  psseq1  3394  psseq2  3395  pssss  3402  pssne  3403  nssinpss  3533  0pss  3625  pssdif  3650  difsnpss  3901  ordelpss  4569  fisseneq  7279  ominf  7280  f1finf1o  7294  fofinf1o  7346  inf3lem2  7540  inf3lem4  7542  infeq5  7548  fin23lem31  8179  isf32lem6  8194  ipolt  14540  lssnle  15261  pgpfaclem2  15595  lspsncv0  16173  islbs3  16182  lbsextlem4  16188  lidlnz  16254  filssufilg  17896  alexsubALTlem4  18034  ppiltx  20913  ex-pss  21689  ch0pss  22900  nepss  25128  dfon2  25362  trelpss  27527  lshpnelb  29467  lshpcmp  29471  lsatssn0  29485  lcvbr3  29506  lsatcv0  29514  lsat0cv  29516  lcvexchlem1  29517  islshpcv  29536  lkrpssN  29646  lkreqN  29653  osumcllem11N  30448  pexmidlem8N  30459  dochsordN  31857  dochsat  31866  dochshpncl  31867  dochexmidlem8  31950  mapdsord  32138
  Copyright terms: Public domain W3C validator