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

Definition df-pss 3369
Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, (ex-pss 22245). Note that (proved in pssirr 3480). Contrast this relationship with the relationship (as defined in df-ss 3367). Other possible definitions are given by dfpss2 3465 and dfpss3 3466. (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 3354 . 2
41, 2wss 3353 . . 3
51, 2wne 2644 . . 3
64, 5wa 360 . 2
73, 6wb 178 1
Colors of variables: wff set class
This definition is referenced by:  dfpss2  3465  psseq1  3467  psseq2  3468  pssss  3475  pssne  3476  nssinpss  3605  0pss  3738  pssdif  3763  difsnpss  4026  ordelpss  4750  fisseneq  7432  ominf  7433  f1finf1o  7447  fofinf1o  7499  inf3lem2  7696  inf3lem4  7698  infeq5  7704  fin23lem31  8337  isf32lem6  8352  ipolt  15107  lssnle  15809  pgpfaclem2  16143  lspsncv0  16721  islbs3  16730  lbsextlem4  16736  lidlnz  16802  filssufilg  18447  alexsubALTlem4  18585  ppiltx  21469  ex-pss  22245  ch0pss  23458  nepss  26005  dfon2  26249  trelpss  28561  lshpnelb  31055  lshpcmp  31059  lsatssn0  31073  lcvbr3  31094  lsatcv0  31102  lsat0cv  31104  lcvexchlem1  31105  islshpcv  31124  lkrpssN  31234  lkreqN  31241  osumcllem11N  32036  pexmidlem8N  32047  dochsordN  33445  dochsat  33454  dochshpncl  33455  dochexmidlem8  33538  mapdsord  33726
  Copyright terms: Public domain W3C validator