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

Definition df-ss 3326
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example,  { 1 ,  2 }  C_  { 1 ,  2 ,  3 } (ex-ss 21723). Note that  A  C_  A (proved in ssid 3359). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 3328). For a more traditional definition, but requiring a dummy variable, see dfss2 3329. Other possible definitions are given by dfss3 3330, dfss4 3567, sspss 3438, ssequn1 3509, ssequn2 3512, sseqin2 3552, and ssdif0 3678. (Contributed by NM, 27-Apr-1994.)
Assertion
Ref Expression
df-ss  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )

Detailed syntax breakdown of Definition df-ss
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2wss 3312 . 2  wff  A  C_  B
41, 2cin 3311 . . 3  class  ( A  i^i  B )
54, 1wceq 1652 . 2  wff  ( A  i^i  B )  =  A
63, 5wb 177 1  wff  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
Colors of variables: wff set class
This definition is referenced by:  dfss  3327  dfss1  3537  inabs  3564  nssinpss  3565  dfrab3ss  3611  disjssun  3677  riinn0  4157  rintn0  4173  ssex  4339  ordtri3or  4605  op1stb  4749  ssdmres  5159  resima2  5170  xpssres  5171  fnimaeq0  5557  fnreseql  5831  curry1  6429  curry2  6432  tpostpos2  6491  sorpssin  6521  tz7.44-2  6656  tz7.44-3  6657  frfnom  6683  ecinxp  6970  infssuni  7388  elfiun  7426  marypha1lem  7429  unxpwdom  7546  cdainf  8061  ackbij1lem16  8104  fin23lem26  8194  isf34lem7  8248  isf34lem6  8249  fpwwe2lem11  8504  fpwwe2lem13  8506  fpwwe2  8507  uzin  10507  iooval2  10938  limsupgle  12259  limsupgre  12263  bitsinv1  12942  bitsres  12973  bitsuz  12974  2prm  13083  dfphi2  13151  ressbas2  13508  ressinbas  13513  ressress  13514  restid2  13646  resscatc  14248  dprdz  15576  dprdcntz2  15584  lmhmlsp  16113  lspdisj2  16187  ressmplbas2  16506  difopn  17086  mretopd  17144  restcld  17224  restopnb  17227  restfpw  17231  neitr  17232  cnrest2  17338  paste  17346  isnrm2  17410  1stccnp  17513  restnlly  17533  lly1stc  17547  kgeni  17557  kgencn3  17578  ptbasfi  17601  hausdiag  17665  qtopval2  17716  qtoprest  17737  filcon  17903  trfil2  17907  trfg  17911  uzrest  17917  trufil  17930  ufileu  17939  fclscf  18045  flimfnfcls  18048  tsmsres  18161  trust  18247  restutopopn  18256  metustfbasOLD  18583  metustfbas  18584  restmetu  18605  xrtgioo  18825  xrsmopn  18831  clsocv  19192  cmetss  19255  ovoliunlem1  19386  difmbl  19425  voliunlem1  19432  volsup2  19485  i1fima  19558  i1fima2  19559  i1fd  19561  itg1addlem5  19580  itg1climres  19594  dvmptid  19831  dvmptc  19832  dvlipcn  19866  dvlip2  19867  dvcnvrelem1  19889  dvcvx  19892  taylthlem1  20277  taylthlem2  20278  psercn  20330  pige3  20413  dvlog  20530  dvcxp1  20614  ppiprm  20922  chtprm  20924  eupares  21685  chm1i  22946  dmdsl3  23806  atssma  23869  dmdbr6ati  23914  imadifxp  24026  sspreima  24045  df1stres  24079  df2ndres  24080  xrge0base  24195  xrge00  24196  esumnul  24431  esumsn  24444  probmeasb  24676  ballotlemfp1  24737  cvmscld  24948  cvmliftmolem1  24956  dfon2lem4  25397  dfrdg2  25407  sspred  25429  nodense  25598  fvline2  26028  mblfinlem2  26191  mblfinlem3  26192  dvreasin  26226  areacirclem2  26228  areacirclem3  26229  topbnd  26264  opnbnd  26265  neibastop1  26325  subspopn  26395  ssbnd  26434  heiborlem3  26459  elrfi  26685  setindtr  27032  fnwe2lem2  27063  lmhmlnmsplit  27100  pmtrmvd  27313  proot1hash  27434  fgraphopab  27444  dmressnsn  27899  fnresfnco  27904  resisresindm  28007  bnj1322  29048  lcvexchlem3  29673  dihglblem5aN  31929
  Copyright terms: Public domain W3C validator