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 3458
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. For example, {1, 2} ⊆ {1, 2, 3} (ex-ss 26425). Note that 𝐴𝐴 (proved in ssid 3491). Contrast this relationship with the relationship 𝐴𝐵 (as will be defined in df-pss 3460). For a more traditional definition, but requiring a dummy variable, see dfss2 3461. Other possible definitions are given by dfss3 3462, dfss4 3723, sspss 3572, ssequn1 3649, ssequn2 3652, sseqin2 3682, and ssdif0 3799. (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 3444 . 2 wff 𝐴𝐵
41, 2cin 3443 . . 3 class (𝐴𝐵)
54, 1wceq 1474 . 2 wff (𝐴𝐵) = 𝐴
63, 5wb 194 1 wff (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  dfss  3459  sseqin2  3682  dfss1OLD  3683  inabs  3720  nssinpss  3721  dfrab3ss  3767  disjssun  3891  riinn0  4429  ssex  4629  op1stb  4765  ssdmres  5231  resima2OLD  5244  dmressnsn  5249  sspred  5495  ordtri3or  5562  fnimaeq0  5811  f0rn0  5886  fnreseql  6118  sorpssin  6717  curry1  7029  curry2  7032  tpostpos2  7133  tz7.44-2  7264  tz7.44-3  7265  frfnom  7291  ecinxp  7583  infssuni  8014  elfiun  8093  marypha1lem  8096  unxpwdom  8251  cdainf  8771  ackbij1lem16  8814  fin23lem26  8904  isf34lem7  8958  isf34lem6  8959  fpwwe2lem11  9215  fpwwe2lem13  9217  fpwwe2  9218  uzin  11456  iooval2  11944  limsupgle  13914  limsupgre  13919  bitsinv1  14870  bitsres  14901  bitsuz  14902  2prm  15123  dfphi2  15199  ressbas2  15646  ressinbas  15651  ressval3d  15652  ressress  15653  restid2  15802  resscatc  16474  pmtrmvd  17595  dprdz  18163  dprdcntz2  18171  lmhmlsp  18778  lspdisj2  18856  ressmplbas2  19184  difopn  20555  mretopd  20613  restcld  20693  restopnb  20696  restfpw  20700  neitr  20701  cnrest2  20807  paste  20815  isnrm2  20879  1stccnp  20982  restnlly  21002  lly1stc  21016  kgeni  21057  kgencn3  21078  ptbasfi  21101  hausdiag  21165  qtopval2  21216  qtoprest  21237  trfil2  21408  trfg  21412  uzrest  21418  trufil  21431  ufileu  21440  fclscf  21546  flimfnfcls  21549  tsmsres  21664  trust  21750  restutopopn  21759  metustfbas  22078  restmetu  22091  xrtgioo  22330  xrsmopn  22336  clsocv  22728  cmetss  22791  ovoliunlem1  22962  difmbl  23004  voliunlem1  23011  volsup2  23065  i1fima  23137  i1fima2  23138  i1fd  23140  itg1addlem5  23159  itg1climres  23173  dvmptid  23412  dvmptc  23413  dvlipcn  23447  dvlip2  23448  dvcnvrelem1  23470  dvcvx  23473  taylthlem1  23829  taylthlem2  23830  psercn  23882  pige3  23971  dvlog  24095  dvcxp1  24179  ppiprm  24577  chtprm  24579  eupares  26251  chm1i  27498  dmdsl3  28357  atssma  28420  dmdbr6ati  28465  imadifxp  28595  fnresin  28611  sspreima  28626  df1stres  28663  df2ndres  28664  xrge0base  28823  xrge00  28824  xrge0slmod  28982  esumnul  29244  esumsnf  29260  baselcarsg  29512  difelcarsg  29516  eulerpartlemgs2  29587  probmeasb  29637  ballotlemfp1  29698  signstres  29834  bnj1322  30003  cvmscld  30365  cvmliftmolem1  30373  mrsubvrs  30529  elmsta  30555  dfon2lem4  30788  dfrdg2  30798  nodense  30934  fvline2  31269  topbnd  31334  opnbnd  31335  neibastop1  31369  bj-restsnss2  32060  mblfinlem3  32484  mblfinlem4  32485  ftc1anclem6  32526  areacirclem1  32536  subspopn  32584  ssbnd  32623  heiborlem3  32648  lcvexchlem3  33207  dihglblem5aN  35465  elrfi  36141  setindtr  36479  fnwe2lem2  36509  lmhmlnmsplit  36545  proot1hash  36674  fgraphopab  36684  iunrelexp0  36890  gneispace  37329  fouriersw  39015  saliincl  39114  saldifcl2  39115  gsumge0cl  39157  sge0sn  39165  sge0tsms  39166  sge0split  39195  caragenunidm  39291  fnresfnco  39748  resisresindm  40224  lidlbas  41804
  Copyright terms: Public domain W3C validator