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

Definition df-pss 3785
Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 27612). Note that ¬ 𝐴𝐴 (proved in pssirr 3905). Contrast this relationship with the relationship 𝐴𝐵 (as defined in df-ss 3783). Other possible definitions are given by dfpss2 3890 and dfpss3 3891. (Contributed by NM, 7-Feb-1996.)
Assertion
Ref Expression
df-pss (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))

Detailed syntax breakdown of Definition df-pss
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2wpss 3770 . 2 wff 𝐴𝐵
41, 2wss 3769 . . 3 wff 𝐴𝐵
51, 2wne 2978 . . 3 wff 𝐴𝐵
64, 5wa 384 . 2 wff (𝐴𝐵𝐴𝐵)
73, 6wb 197 1 wff (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  dfpss2  3890  psseq1  3892  psseq2  3893  pssss  3900  pssne  3901  nssinpss  4058  pssdif  4146  0pss  4211  difsnpss  4528  ordelpss  5964  fisseneq  8406  ominf  8407  f1finf1o  8422  fofinf1o  8476  inf3lem2  8769  inf3lem4  8771  infeq5  8777  fin23lem31  9446  isf32lem6  9461  ipolt  17360  lssnle  18284  pgpfaclem2  18679  lspsncv0  19350  lspsncv0OLD  19351  islbs3  19360  lbsextlem4  19366  lidlnz  19433  filssufilg  21924  alexsubALTlem4  22063  ppiltx  25113  ex-pss  27612  ch0pss  28628  nepss  31916  dfon2  32012  relowlpssretop  33523  finxpreclem3  33541  fin2solem  33703  lshpnelb  34759  lshpcmp  34763  lsatssn0  34777  lcvbr3  34798  lsatcv0  34806  lsat0cv  34808  lcvexchlem1  34809  islshpcv  34828  lkrpssN  34938  lkreqN  34945  osumcllem11N  35741  pexmidlem8N  35752  dochsordN  37149  dochsat  37158  dochshpncl  37159  dochexmidlem8  37242  mapdsord  37430  psspwb  37746  xppss12  37747  trelpss  39151  isomenndlem  41220  lvecpsslmod  42858
  Copyright terms: Public domain W3C validator