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

Definition df-pss 3338
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 21738). Note that  -.  A  C.  A (proved in pssirr 3449). Contrast this relationship with the relationship  A 
C_  B (as defined in df-ss 3336). Other possible definitions are given by dfpss2 3434 and dfpss3 3435. (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 3323 . 2  wff  A  C.  B
41, 2wss 3322 . . 3  wff  A  C_  B
51, 2wne 2601 . . 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  3434  psseq1  3436  psseq2  3437  pssss  3444  pssne  3445  nssinpss  3575  0pss  3667  pssdif  3692  difsnpss  3943  ordelpss  4611  fisseneq  7322  ominf  7323  f1finf1o  7337  fofinf1o  7389  inf3lem2  7586  inf3lem4  7588  infeq5  7594  fin23lem31  8225  isf32lem6  8240  ipolt  14587  lssnle  15308  pgpfaclem2  15642  lspsncv0  16220  islbs3  16229  lbsextlem4  16235  lidlnz  16301  filssufilg  17945  alexsubALTlem4  18083  ppiltx  20962  ex-pss  21738  ch0pss  22949  nepss  25177  dfon2  25421  trelpss  27638  lshpnelb  29844  lshpcmp  29848  lsatssn0  29862  lcvbr3  29883  lsatcv0  29891  lsat0cv  29893  lcvexchlem1  29894  islshpcv  29913  lkrpssN  30023  lkreqN  30030  osumcllem11N  30825  pexmidlem8N  30836  dochsordN  32234  dochsat  32243  dochshpncl  32244  dochexmidlem8  32327  mapdsord  32515
  Copyright terms: Public domain W3C validator