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

Theorem eqss 3195
Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eqss  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )

Proof of Theorem eqss
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 albiim 1598 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  <->  ( A. x
( x  e.  A  ->  x  e.  B )  /\  A. x ( x  e.  B  ->  x  e.  A )
) )
2 dfcleq 2278 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3170 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3170 . . 3  |-  ( B 
C_  A  <->  A. x
( x  e.  B  ->  x  e.  A ) )
53, 4anbi12i 678 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  <->  ( A. x ( x  e.  A  ->  x  e.  B )  /\  A. x ( x  e.  B  ->  x  e.  A ) ) )
61, 2, 53bitr4i 268 1  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527    = wceq 1623    e. wcel 1685    C_ wss 3153
This theorem is referenced by:  eqssi  3196  eqssd  3197  sseq1  3200  sseq2  3201  eqimss  3231  dfpss3  3263  uneqin  3421  ss0b  3485  vss  3492  pssdifn0  3516  pwpw0  3764  sssn  3773  ssunsn  3775  pwsnALT  3823  unidif  3860  ssunieq  3861  uniintsn  3900  iuneq1  3919  iuneq2  3922  iunxdif2  3951  ssext  4227  pweqb  4229  eqopab2b  4293  pwun  4301  soeq2  4333  ordtri4  4428  oneqmini  4442  iunpw  4569  orduniorsuc  4620  tfi  4643  eqrel  4776  eqrelrel  4787  coeq1  4840  coeq2  4841  cnveq  4854  dmeq  4878  relssres  4991  xp11  5110  ssrnres  5115  fnres  5326  eqfnfv3  5586  fneqeql2  5596  dff3  5635  fconst4  5698  f1imaeq  5751  eqoprab2b  5868  fo1stres  6105  fo2ndres  6106  tz7.49  6453  oawordeulem  6548  nnacan  6622  nnmcan  6628  ixpeq2  6826  sbthlem3  6969  isinf  7072  ordunifi  7103  inficl  7174  rankr1c  7489  rankc1  7538  iscard  7604  iscard2  7605  carden2  7616  aleph11  7707  cardaleph  7712  alephinit  7718  dfac12a  7770  cflm  7872  cfslb2n  7890  dfacfin7  8021  wrdeq  11420  isumltss  12303  rpnnen2  12500  isprm2  12762  mrcidb2  13516  iscyggen2  15164  iscyg3  15169  lssle0  15703  islpir2  15999  iscss2  16582  ishil2  16615  bastop1  16727  epttop  16742  iscld4  16798  0ntr  16804  opnneiid  16859  isperf2  16879  cnntr  17000  ist1-3  17073  perfcls  17089  cmpfi  17131  iscon2  17136  dfcon2  17141  snfil  17555  filcon  17574  ufileu  17610  alexsubALTlem4  17740  metequiv  18051  shlesb1i  21961  shle0  22017  orthin  22021  chcon2i  22039  chcon3i  22041  chlejb1i  22051  chabs2  22092  h1datomi  22156  cmbr4i  22176  osumcor2i  22219  pjjsi  22275  pjin2i  22769  stcltr2i  22851  mdbr2  22872  dmdbr2  22879  mdsl2i  22898  mdsl2bi  22899  mdslmd3i  22908  chrelat4i  22949  sumdmdlem2  22995  dmdbr5ati  22998  dfon2lem9  23551  wfrlem8  23667  idsset  23841  domfldrefc  24467  ranfldrefc  24468  domintrefb  24473  twsymr  24488  sssu  24552  inposet  24689  dfps2  24700  hdrmp  25117  fneval  25698  equivtotbnd  25913  heiborlem10  25955  isnacs2  26192  mrefg3  26194  pmap11  29230  dia11N  30517  dia2dimlem5  30537  dib11N  30629  dih11  30734  dihglblem6  30809  doch11  30842  mapd11  31108  mapdcnv11N  31128
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator