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 3623
Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 27415). Note that ¬ 𝐴𝐴 (proved in pssirr 3740). Contrast this relationship with the relationship 𝐴𝐵 (as defined in df-ss 3621). Other possible definitions are given by dfpss2 3725 and dfpss3 3726. (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 3608 . 2 wff 𝐴𝐵
41, 2wss 3607 . . 3 wff 𝐴𝐵
51, 2wne 2823 . . 3 wff 𝐴𝐵
64, 5wa 383 . 2 wff (𝐴𝐵𝐴𝐵)
73, 6wb 196 1 wff (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  dfpss2  3725  psseq1  3727  psseq2  3728  pssss  3735  pssne  3736  nssinpss  3889  pssdif  3978  0pss  4046  difsnpss  4370  ordelpss  5789  fisseneq  8212  ominf  8213  f1finf1o  8228  fofinf1o  8282  inf3lem2  8564  inf3lem4  8566  infeq5  8572  fin23lem31  9203  isf32lem6  9218  ipolt  17206  lssnle  18133  pgpfaclem2  18527  lspsncv0  19194  islbs3  19203  lbsextlem4  19209  lidlnz  19276  filssufilg  21762  alexsubALTlem4  21901  ppiltx  24948  ex-pss  27415  ch0pss  28432  nepss  31725  dfon2  31821  relowlpssretop  33342  finxpreclem3  33360  fin2solem  33525  lshpnelb  34589  lshpcmp  34593  lsatssn0  34607  lcvbr3  34628  lsatcv0  34636  lsat0cv  34638  lcvexchlem1  34639  islshpcv  34658  lkrpssN  34768  lkreqN  34775  osumcllem11N  35570  pexmidlem8N  35581  dochsordN  36980  dochsat  36989  dochshpncl  36990  dochexmidlem8  37073  mapdsord  37261  trelpss  38976  isomenndlem  41065  lvecpsslmod  42621
  Copyright terms: Public domain W3C validator