MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfss3 Structured version   Unicode version

Theorem dfss3 3340
Description: Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)
Assertion
Ref Expression
dfss3  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
Distinct variable groups:    x, A    x, B

Proof of Theorem dfss3
StepHypRef Expression
1 dfss2 3339 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
2 df-ral 2712 . 2  |-  ( A. x  e.  A  x  e.  B  <->  A. x ( x  e.  A  ->  x  e.  B ) )
31, 2bitr4i 245 1  |-  ( A 
C_  B  <->  A. x  e.  A  x  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550    e. wcel 1726   A.wral 2707    C_ wss 3322
This theorem is referenced by:  ssrab  3423  eqsn  3962  uni0b  4042  uni0c  4043  ssint  4068  ssiinf  4142  sspwuni  4178  dftr3  4308  wefrc  4578  ordunisssuc  4686  elpwunsn  4759  tfis  4836  rninxp  5312  fnres  5563  eqfnfv3  5831  funimass3  5848  ffvresb  5902  smogt  6631  unifi  7397  unifi2  7398  fissuni  7413  fipreima  7414  cantnf  7651  tz9.12lem3  7717  r1elss  7734  rankval3b  7754  rankonidlem  7756  bndrank  7769  iscard  7864  cfub  8131  cflm  8132  fin1a2s  8296  dcomex  8329  ttukeylem6  8396  unirnfdomd  8444  alephreg  8459  tskord  8657  gruuni  8677  intgru  8691  grudomon  8694  axgroth3  8708  suplem1pr  8931  supexpr  8933  supsr  8989  hashfun  11702  4sqlem19  13333  imasaddfnlem  13755  imasvscafn  13764  setcepi  14245  acsfiindd  14605  sylow2blem3  15258  sylow3lem6  15268  efgval2  15358  iscyggen2  15493  iscyg3  15498  issubdrg  15895  isdomn2  16361  ishil2  16948  rintopn  16984  isbasis2g  17015  tgval2  17023  eltg2b  17026  tgss2  17054  basgen2  17056  bastop1  17060  intcld  17106  unicld  17112  isclo  17153  isclo2  17154  neips  17179  opnnei  17186  neiptopnei  17198  isperf3  17219  ssidcn  17321  ist1-3  17415  cmpcov2  17455  cmpsub  17465  2ndcdisj2  17522  txkgen  17686  xkoinjcn  17721  tgqtop  17746  flimopn  18009  flfnei  18025  tmdcn2  18121  divstgplem  18152  cfil3i  19224  cmetcaulem  19243  ovolfioo  19366  ovolficc  19367  ovolicc2lem4  19418  opnmblALT  19497  xrlimcnp  20809  ubthlem1  22374  hasheuni  24477  dmvlsiga  24514  cvmlift2lem1  24991  cvmlift2lem12  25003  setinds  25407  tfisg  25481  wfisg  25486  frinsg  25522  isfne4  26351  isfne2  26353  isfne3  26354  neibastop2lem  26391  filnetlem4  26412  nninfnub  26457  unichnidl  26643  ispridl2  26650  isnacs2  26762  setindtrs  27098  dford3lem2  27100  dford3  27101  stoweidlem31  27758  stoweidlem39  27766  pmapglb  30629  hdmapoc  32794
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2712  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator