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

Definition df-ss 3166
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example,  { 1 ,  2 }  C_  { 1 ,  2 ,  3 } (ex-ss 20814). Note that  A  C_  A (proved in ssid 3197). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 3168). For a more traditional definition, but requiring a dummy variable, see dfss2 3169. Other possible definitions are given by dfss3 3170, dfss4 3403, sspss 3275, ssequn1 3345, ssequn2 3348, sseqin2 3388, and ssdif0 3513. (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 3152 . 2  wff  A  C_  B
41, 2cin 3151 . . 3  class  ( A  i^i  B )
54, 1wceq 1623 . 2  wff  ( A  i^i  B )  =  A
63, 5wb 176 1  wff  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
Colors of variables: wff set class
This definition is referenced by:  dfss  3167  dfss1  3373  inabs  3400  nssinpss  3401  dfrab3ss  3446  disjssun  3512  riinn0  3976  rintn0  3992  ssex  4158  ordtri3or  4424  op1stb  4569  ssdmres  4977  resima2  4988  xpssres  4989  fnimaeq0  5365  fnreseql  5635  curry1  6210  curry2  6213  tpostpos2  6255  sorpssin  6285  tz7.44-2  6420  tz7.44-3  6421  frfnom  6447  ecinxp  6734  elfiun  7183  marypha1lem  7186  unxpwdom  7303  cdainf  7818  ackbij1lem16  7861  fin23lem26  7951  isf34lem7  8005  isf34lem6  8006  fpwwe2lem11  8262  fpwwe2lem13  8264  fpwwe2  8265  uzin  10260  iooval2  10689  limsupgle  11951  limsupgre  11955  incexclem  12295  incexc  12296  bitsinv1  12633  bitsres  12664  bitsuz  12665  2prm  12774  dfphi2  12842  ressbas2  13199  ressinbas  13204  ressress  13205  restid2  13335  resscatc  13937  dprdz  15265  dprdcntz2  15273  lmhmlsp  15806  lspdisj2  15880  ressmplbas2  16199  difopn  16771  mretopd  16829  restcld  16903  restopnb  16906  restfpw  16910  cnrest2  17014  paste  17022  isnrm2  17086  1stccnp  17188  restnlly  17208  lly1stc  17222  kgeni  17232  kgencn3  17253  ptbasfi  17276  hausdiag  17339  qtopval2  17387  qtoprest  17408  filcon  17578  trfil2  17582  trfg  17586  uzrest  17592  trufil  17605  ufileu  17614  fclscf  17720  flimfnfcls  17723  tsmsres  17826  xrtgioo  18312  xrsmopn  18318  clsocv  18677  cmetss  18740  ovoliunlem1  18861  difmbl  18900  voliunlem1  18907  volsup2  18960  i1fima  19033  i1fima2  19034  i1fd  19036  itg1addlem5  19055  itg1climres  19069  dvmptid  19306  dvmptc  19307  dvlipcn  19341  dvlip2  19342  dvcnvrelem1  19364  dvcvx  19367  taylthlem1  19752  taylthlem2  19753  psercn  19802  pige3  19885  dvlog  19998  dvcxp1  20082  ppiprm  20389  chtprm  20391  chm1i  22035  dmdsl3  22895  atssma  22958  dmdbr6ati  23003  ballotlemfp1  23050  ballotlemfmpn  23053  sspreima  23210  df1stres  23243  df2ndres  23244  xrge0base  23310  xrge00  23311  esumnul  23427  esumsn  23437  totprobd  23629  probmeasb  23633  cvmscld  23804  cvmliftmolem1  23812  eupares  23899  dfon2lem4  24142  dfrdg2  24152  sspred  24174  nodense  24343  fvline2  24769  dvreasin  24923  areacirclem2  24925  areacirclem3  24926  isunscov  25074  domrancur1b  25200  domrancur1c  25202  basexre  25522  islimrs4  25582  topbnd  26242  opnbnd  26243  neibastop1  26308  subspopn  26466  ssbnd  26512  heiborlem3  26537  elrfi  26769  setindtr  27117  fnwe2lem2  27148  lmhmlnmsplit  27185  pmtrmvd  27398  proot1hash  27519  fgraphopab  27529  dmressnsn  27983  fnresfnco  27989  funcoressn  27990  funressnfv  27991  bnj1322  28855  lcvexchlem3  29226  dihglblem5aN  31482
  Copyright terms: Public domain W3C validator