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

Definition df-pss 3325
Description: Define proper subclass relationship between two classes. Definition 5.9 ?Error: 1 , 2 } C. { 1 , 2 , 3 } ^ This math symbol is not active (i.e. was not declared in this scope). of [TakeutiZaring] p. 17. For example, {1,2}C.{1,2,3} (ex-pss 21787). Note that (proved in pssirr 3436). Contrast this relationship with the relationship (as defined in df-ss 3323). Other possible definitions are given by dfpss2 3421 and dfpss3 3422. (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 3310 . 2
41, 2wss 3309 . . 3
51, 2wne 2606 . . 3
64, 5wa 360 . 2
73, 6wb 178 1
Colors of variables: wff set class
This definition is referenced by:  dfpss2  3421  psseq1  3423  psseq2  3424  pssss  3431  pssne  3432  nssinpss  3561  0pss  3691  pssdif  3716  difsnpss  3969  ordelpss  4650  fisseneq  7369  ominf  7370  f1finf1o  7384  fofinf1o  7436  inf3lem2  7633  inf3lem4  7635  infeq5  7641  fin23lem31  8274  isf32lem6  8289  ipolt  14636  lssnle  15357  pgpfaclem2  15691  lspsncv0  16269  islbs3  16278  lbsextlem4  16284  lidlnz  16350  filssufilg  17994  alexsubALTlem4  18132  ppiltx  21011  ex-pss  21787  ch0pss  22998  nepss  25279  dfon2  25523  trelpss  27814  lshpnelb  30022  lshpcmp  30026  lsatssn0  30040  lcvbr3  30061  lsatcv0  30069  lsat0cv  30071  lcvexchlem1  30072  islshpcv  30091  lkrpssN  30201  lkreqN  30208  osumcllem11N  31003  pexmidlem8N  31014  dochsordN  32412  dochsat  32421  dochshpncl  32422  dochexmidlem8  32505  mapdsord  32693
  Copyright terms: Public domain W3C validator