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

Definition df-pss 3381
Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, (ex-pss 22757). Note that (proved in pssirr 3493). Contrast this relationship with the relationship (as defined in df-ss 3379). Other possible definitions are given by dfpss2 3478 and dfpss3 3479. (Contributed by NM, 7-Feb-1996.)
Assertion
Ref Expression
df-pss

Detailed syntax breakdown of Definition df-pss
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2wpss 3366 . 2
41, 2wss 3365 . . 3
51, 2wne 2652 . . 3
64, 5wa 360 . 2
73, 6wb 178 1
Colors of variables: wff set class
This definition is referenced by:  dfpss2  3478  psseq1  3480  psseq2  3481  pssss  3488  pssne  3489  nssinpss  3618  0pss  3751  pssdif  3776  difsnpss  4041  ordelpss  4768  fisseneq  7485  ominf  7486  f1finf1o  7500  fofinf1o  7553  inf3lem2  7751  inf3lem4  7753  infeq5  7759  fin23lem31  8394  isf32lem6  8409  ipolt  15170  lssnle  15915  pgpfaclem2  16255  lspsncv0  16841  islbs3  16850  lbsextlem4  16856  lidlnz  16924  filssufilg  18958  alexsubALTlem4  19096  ppiltx  21981  ex-pss  22757  ch0pss  23970  nepss  26514  dfon2  26758  trelpss  28886  lshpnelb  31332  lshpcmp  31336  lsatssn0  31350  lcvbr3  31371  lsatcv0  31379  lsat0cv  31381  lcvexchlem1  31382  islshpcv  31401  lkrpssN  31511  lkreqN  31518  osumcllem11N  32313  pexmidlem8N  32324  dochsordN  33722  dochsat  33731  dochshpncl  33732  dochexmidlem8  33815  mapdsord  34003
  Copyright terms: Public domain W3C validator