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

Definition df-pss 3491
Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, (ex-pss 25149). Note that (proved in pssirr 3603). Contrast this relationship with the relationship (as defined in df-ss 3489). Other possible definitions are given by dfpss2 3588 and dfpss3 3589. (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 3476 . 2
41, 2wss 3475 . . 3
51, 2wne 2652 . . 3
64, 5wa 369 . 2
73, 6wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  dfpss2  3588  psseq1  3590  psseq2  3591  pssss  3598  pssne  3599  nssinpss  3729  0pss  3864  pssdif  3889  difsnpss  4173  ordelpss  4911  fisseneq  7751  ominf  7752  f1finf1o  7766  fofinf1o  7821  inf3lem2  8067  inf3lem4  8069  infeq5  8075  fin23lem31  8744  isf32lem6  8759  ipolt  15789  lssnle  16692  pgpfaclem2  17133  lspsncv0  17792  islbs3  17801  lbsextlem4  17807  lidlnz  17876  filssufilg  20412  alexsubALTlem4  20550  ppiltx  23451  ex-pss  25149  ch0pss  26363  nepss  29095  dfon2  29224  fin2solem  30039  trelpss  31364  lvecpsslmod  33108  lshpnelb  34709  lshpcmp  34713  lsatssn0  34727  lcvbr3  34748  lsatcv0  34756  lsat0cv  34758  lcvexchlem1  34759  islshpcv  34778  lkrpssN  34888  lkreqN  34895  osumcllem11N  35690  pexmidlem8N  35701  dochsordN  37101  dochsat  37110  dochshpncl  37111  dochexmidlem8  37194  mapdsord  37382
  Copyright terms: Public domain W3C validator