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 3574
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 27172). Note that 𝐴𝐴 (proved in ssid 3609). Contrast this relationship with the relationship 𝐴𝐵 (as will be defined in df-pss 3576). For a more traditional definition, but requiring a dummy variable, see dfss2 3577. Other possible definitions are given by dfss3 3578, dfss4 3842, sspss 3690, ssequn1 3767, ssequn2 3770, sseqin2 3801, and ssdif0 3922. (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 3560 . 2 wff 𝐴𝐵
41, 2cin 3559 . . 3 class (𝐴𝐵)
54, 1wceq 1480 . 2 wff (𝐴𝐵) = 𝐴
63, 5wb 196 1 wff (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  dfss  3575  sseqin2  3801  dfss1OLD  3802  inabs  3839  nssinpss  3840  dfrab3ss  3887  disjssun  4014  riinn0  4568  ssex  4772  op1stb  4911  ssdmres  5389  resima2OLD  5402  dmressnsn  5407  sspred  5657  ordtri3or  5724  fnimaeq0  5980  f0rn0  6057  fnreseql  6293  sorpssin  6910  curry1  7229  curry2  7232  tpostpos2  7333  tz7.44-2  7463  tz7.44-3  7464  frfnom  7490  ecinxp  7782  infssuni  8217  elfiun  8296  marypha1lem  8299  unxpwdom  8454  cdainf  8974  ackbij1lem16  9017  fin23lem26  9107  isf34lem7  9161  isf34lem6  9162  fpwwe2lem11  9422  fpwwe2lem13  9424  fpwwe2  9425  uzin  11680  iooval2  12166  limsupgle  14158  limsupgre  14162  bitsinv1  15107  bitsres  15138  bitsuz  15139  2prm  15348  dfphi2  15422  ressbas2  15871  ressinbas  15876  ressval3d  15877  ressress  15878  restid2  16031  resscatc  16695  pmtrmvd  17816  dprdz  18369  dprdcntz2  18377  lmhmlsp  18989  lspdisj2  19067  ressmplbas2  19395  difopn  20778  mretopd  20836  restcld  20916  restopnb  20919  restfpw  20923  neitr  20924  cnrest2  21030  paste  21038  isnrm2  21102  1stccnp  21205  restnlly  21225  lly1stc  21239  kgeni  21280  kgencn3  21301  ptbasfi  21324  hausdiag  21388  qtopval2  21439  qtoprest  21460  trfil2  21631  trfg  21635  uzrest  21641  trufil  21654  ufileu  21663  fclscf  21769  flimfnfcls  21772  tsmsres  21887  trust  21973  restutopopn  21982  metustfbas  22302  restmetu  22315  xrtgioo  22549  xrsmopn  22555  clsocv  22989  cmetss  23053  ovoliunlem1  23210  difmbl  23251  voliunlem1  23258  volsup2  23313  i1fima  23385  i1fima2  23386  i1fd  23388  itg1addlem5  23407  itg1climres  23421  dvmptid  23660  dvmptc  23661  dvlipcn  23695  dvlip2  23696  dvcnvrelem1  23718  dvcvx  23721  taylthlem1  24065  taylthlem2  24066  psercn  24118  pige3  24207  dvlog  24331  dvcxp1  24415  ppiprm  24811  chtprm  24813  chm1i  28203  dmdsl3  29062  atssma  29125  dmdbr6ati  29170  imadifxp  29300  fnresin  29315  sspreima  29330  df1stres  29365  df2ndres  29366  xrge0base  29512  xrge00  29513  xrge0slmod  29671  esumnul  29933  esumsnf  29949  baselcarsg  30191  difelcarsg  30195  eulerpartlemgs2  30265  probmeasb  30315  ballotlemfp1  30376  signstres  30474  ftc2re  30492  bnj1322  30654  cvmscld  31016  cvmliftmolem1  31024  mrsubvrs  31180  elmsta  31206  dfon2lem4  31445  dfrdg2  31455  nodense  31605  nosires  31630  fvline2  31948  topbnd  32014  opnbnd  32015  neibastop1  32049  bj-disj2r  32713  bj-restsnss2  32727  mblfinlem3  33119  mblfinlem4  33120  ftc1anclem6  33161  areacirclem1  33171  subspopn  33219  ssbnd  33258  heiborlem3  33283  lcvexchlem3  33842  dihglblem5aN  36100  elrfi  36776  setindtr  37110  fnwe2lem2  37140  lmhmlnmsplit  37176  proot1hash  37298  fgraphopab  37308  iunrelexp0  37514  gneispace  37953  uzinico2  39235  limsupval3  39360  limsupvaluz  39376  fouriersw  39785  saliincl  39882  saldifcl2  39883  gsumge0cl  39925  sge0sn  39933  sge0tsms  39934  sge0split  39963  caragenunidm  40059  fnresfnco  40540  lidlbas  41241
  Copyright terms: Public domain W3C validator