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 3554
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 26676). Note that 𝐴𝐴 (proved in ssid 3587). Contrast this relationship with the relationship 𝐴𝐵 (as will be defined in df-pss 3556). For a more traditional definition, but requiring a dummy variable, see dfss2 3557. Other possible definitions are given by dfss3 3558, dfss4 3820, sspss 3668, ssequn1 3745, ssequn2 3748, sseqin2 3779, and ssdif0 3896. (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 3540 . 2 wff 𝐴𝐵
41, 2cin 3539 . . 3 class (𝐴𝐵)
54, 1wceq 1475 . 2 wff (𝐴𝐵) = 𝐴
63, 5wb 195 1 wff (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  dfss  3555  sseqin2  3779  dfss1OLD  3780  inabs  3817  nssinpss  3818  dfrab3ss  3864  disjssun  3988  riinn0  4531  ssex  4730  op1stb  4867  ssdmres  5340  resima2OLD  5353  dmressnsn  5358  sspred  5605  ordtri3or  5672  fnimaeq0  5926  f0rn0  6003  fnreseql  6235  sorpssin  6843  curry1  7156  curry2  7159  tpostpos2  7260  tz7.44-2  7390  tz7.44-3  7391  frfnom  7417  ecinxp  7709  infssuni  8140  elfiun  8219  marypha1lem  8222  unxpwdom  8377  cdainf  8897  ackbij1lem16  8940  fin23lem26  9030  isf34lem7  9084  isf34lem6  9085  fpwwe2lem11  9341  fpwwe2lem13  9343  fpwwe2  9344  uzin  11596  iooval2  12079  limsupgle  14056  limsupgre  14060  bitsinv1  15002  bitsres  15033  bitsuz  15034  2prm  15243  dfphi2  15317  ressbas2  15758  ressinbas  15763  ressval3d  15764  ressress  15765  restid2  15914  resscatc  16578  pmtrmvd  17699  dprdz  18252  dprdcntz2  18260  lmhmlsp  18870  lspdisj2  18948  ressmplbas2  19276  difopn  20648  mretopd  20706  restcld  20786  restopnb  20789  restfpw  20793  neitr  20794  cnrest2  20900  paste  20908  isnrm2  20972  1stccnp  21075  restnlly  21095  lly1stc  21109  kgeni  21150  kgencn3  21171  ptbasfi  21194  hausdiag  21258  qtopval2  21309  qtoprest  21330  trfil2  21501  trfg  21505  uzrest  21511  trufil  21524  ufileu  21533  fclscf  21639  flimfnfcls  21642  tsmsres  21757  trust  21843  restutopopn  21852  metustfbas  22172  restmetu  22185  xrtgioo  22417  xrsmopn  22423  clsocv  22857  cmetss  22921  ovoliunlem1  23077  difmbl  23118  voliunlem1  23125  volsup2  23179  i1fima  23251  i1fima2  23252  i1fd  23254  itg1addlem5  23273  itg1climres  23287  dvmptid  23526  dvmptc  23527  dvlipcn  23561  dvlip2  23562  dvcnvrelem1  23584  dvcvx  23587  taylthlem1  23931  taylthlem2  23932  psercn  23984  pige3  24073  dvlog  24197  dvcxp1  24281  ppiprm  24677  chtprm  24679  eupares  26502  chm1i  27699  dmdsl3  28558  atssma  28621  dmdbr6ati  28666  imadifxp  28796  fnresin  28812  sspreima  28827  df1stres  28864  df2ndres  28865  xrge0base  29016  xrge00  29017  xrge0slmod  29175  esumnul  29437  esumsnf  29453  baselcarsg  29695  difelcarsg  29699  eulerpartlemgs2  29769  probmeasb  29819  ballotlemfp1  29880  signstres  29978  bnj1322  30147  cvmscld  30509  cvmliftmolem1  30517  mrsubvrs  30673  elmsta  30699  dfon2lem4  30935  dfrdg2  30945  nodense  31088  fvline2  31423  topbnd  31489  opnbnd  31490  neibastop1  31524  bj-restsnss2  32218  mblfinlem3  32618  mblfinlem4  32619  ftc1anclem6  32660  areacirclem1  32670  subspopn  32718  ssbnd  32757  heiborlem3  32782  lcvexchlem3  33341  dihglblem5aN  35599  elrfi  36275  setindtr  36609  fnwe2lem2  36639  lmhmlnmsplit  36675  proot1hash  36797  fgraphopab  36807  iunrelexp0  37013  gneispace  37452  fouriersw  39124  saliincl  39221  saldifcl2  39222  gsumge0cl  39264  sge0sn  39272  sge0tsms  39273  sge0split  39302  caragenunidm  39398  fnresfnco  39855  resisresindm  40320  lidlbas  41713
  Copyright terms: Public domain W3C validator