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

Definition df-ss 3901
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 28215). Note that 𝐴𝐴 (proved in ssid 3940). Contrast this relationship with the relationship 𝐴𝐵 (as will be defined in df-pss 3903). For a more traditional definition, but requiring a dummy variable, see dfss2 3904. Other possible definitions are given by dfss3 3906, dfss4 4188, sspss 4030, ssequn1 4110, ssequn2 4113, sseqin2 4145, and ssdif0 4280.

We prefer the label "ss" ("subset") for , despite the fact that it applies to classes. It is much more common to refer to this as the subset relation than subclass, especially since most of the time the arguments are in fact sets (and for pragmatic reasons we don't want to need to use different operations for sets). The way set.mm is set up, many things are technically classes despite morally (and provably) being sets, like 1 (cf. df-1 10538 and 1ex 10630) or ( cf. df-r 10540 and reex 10621). This has to do with the fact that there are no "set expressions": classes are expressions but there are only set variables in set.mm (cf. https://us.metamath.org/downloads/grammar-ambiguity.txt 10621). This is why we use both for subclass relations and for subset relations and call it "subset". (Contributed by NM, 27-Apr-1994.)

Assertion
Ref Expression
df-ss (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)

Detailed syntax breakdown of Definition df-ss
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2wss 3884 . 2 wff 𝐴𝐵
41, 2cin 3883 . . 3 class (𝐴𝐵)
54, 1wceq 1538 . 2 wff (𝐴𝐵) = 𝐴
63, 5wb 209 1 wff (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  dfss  3902  ss2abdv  3994  sseqin2  4145  dfss7  4170  inabs  4185  nssinpss  4186  dfrab3ss  4236  disjssun  4378  riinn0  4971  ssex  5192  op1stb  5331  ssdmres  5845  dmressnsn  5864  sspred  6128  ordtri3or  6195  fnimaeq0  6457  f0rn0  6542  fnreseql  6799  sorpssin  7441  curry1  7786  curry2  7789  tpostpos2  7900  tz7.44-2  8030  tz7.44-3  8031  frfnom  8057  ecinxp  8359  infssuni  8803  elfiun  8882  marypha1lem  8885  unxpwdom  9041  djuinf  9603  ackbij1lem16  9650  fin23lem26  9740  isf34lem7  9794  isf34lem6  9795  fpwwe2lem11  10055  fpwwe2lem13  10057  fpwwe2  10058  uzin  12270  iooval2  12763  limsupgle  14829  limsupgre  14833  bitsinv1  15784  bitsres  15815  bitsuz  15816  2prm  16029  dfphi2  16104  ressbas2  16550  ressinbas  16555  ressval3d  16556  ressress  16557  restid2  16699  resscatc  17360  symgvalstruct  18520  pmtrmvd  18579  dprdz  19148  dprdcntz2  19156  lmhmlsp  19817  lspdisj2  19895  ressmplbas2  20698  difopn  21642  mretopd  21700  restcld  21780  restopnb  21783  restfpw  21787  neitr  21788  cnrest2  21894  paste  21902  isnrm2  21966  1stccnp  22070  restnlly  22090  lly1stc  22104  kgeni  22145  kgencn3  22166  ptbasfi  22189  hausdiag  22253  qtopval2  22304  qtoprest  22325  trfil2  22495  trfg  22499  uzrest  22505  trufil  22518  ufileu  22527  fclscf  22633  flimfnfcls  22636  tsmsres  22752  trust  22838  restutopopn  22847  metustfbas  23167  restmetu  23180  xrtgioo  23414  xrsmopn  23420  clsocv  23857  cmetss  23923  ovoliunlem1  24109  difmbl  24150  voliunlem1  24157  volsup2  24212  i1fima  24285  i1fima2  24286  i1fd  24288  itg1addlem5  24307  itg1climres  24321  dvmptid  24563  dvmptc  24564  dvlipcn  24600  dvlip2  24601  dvcnvrelem1  24623  dvcvx  24626  taylthlem1  24971  taylthlem2  24972  psercn  25024  pige3ALT  25115  dvlog  25245  dvcxp1  25332  ppiprm  25739  chtprm  25741  chm1i  29242  dmdsl3  30101  atssma  30164  dmdbr6ati  30209  imadifxp  30367  fnresin  30388  sspreima  30409  preimane  30436  fnpreimac  30437  mptprop  30461  df1stres  30466  df2ndres  30467  preiman0  30472  xrge0base  30722  xrge00  30723  gsumhashmul  30744  cycpm2tr  30814  xrge0slmod  30971  fldexttr  31136  zarcmplem  31234  esumnul  31415  esumsnf  31431  baselcarsg  31672  difelcarsg  31676  eulerpartlemgs2  31746  probmeasb  31796  ballotlemfp1  31857  signstres  31953  ftc2re  31977  bnj1322  32202  cvmscld  32628  cvmliftmolem1  32636  mrsubvrs  32877  elmsta  32903  dfon2lem4  33139  dfrdg2  33148  nolesgn2ores  33287  nodense  33304  nosupres  33315  nosupbnd2lem1  33323  fvline2  33715  topbnd  33780  opnbnd  33781  neibastop1  33815  bj-disj2r  34459  bj-restsnss2  34494  bj-0int  34511  bj-prmoore  34525  bj-inexeqex  34564  bj-idreseq  34572  mblfinlem3  35089  mblfinlem4  35090  ftc1anclem6  35128  areacirclem1  35138  subspopn  35183  ssbnd  35219  heiborlem3  35244  lcvexchlem3  36325  dihglblem5aN  38581  elrfi  39622  setindtr  39952  fnwe2lem2  39982  lmhmlnmsplit  40018  proot1hash  40131  fgraphopab  40141  iunrelexp0  40390  gneispace  40824  uzinico2  42186  limsupval3  42321  limsupvaluz  42337  liminfval5  42394  fouriersw  42860  saliincl  42954  saldifcl2  42955  gsumge0cl  42997  sge0sn  43005  sge0tsms  43006  sge0split  43035  caragenunidm  43134  fnresfnco  43620  imaelsetpreimafv  43899  lidlbas  44534
  Copyright terms: Public domain W3C validator