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  27863  lshpcmp  27867  lsatssn0  27881  lcvbr3  27902  lsatcv0  27910  lsat0cv  27912  lcvexchlem1  27913  islshpcv  27932  lkrpssN  28042  lkreqN  28049  osumcllem11N  28844  pexmidlem8N  28855  dochsordN  30253  dochsat  30262  dochshpncl  30263  dochexmidlem8  30346  mapdsord  30534
  Copyright terms: Public domain W3C validator