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

Theorem eqss 3136
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
StepHypRef Expression
1 albiim 1612 . 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 2250 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
3 dfss2 3111 . . 3  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
4 dfss2 3111 . . 3  |-  ( B 
C_  A  <->  A. x
( x  e.  B  ->  x  e.  A ) )
53, 4anbi12i 681 . 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 270 1  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360   A.wal 1532    = wceq 1619    e. wcel 1621    C_ wss 3094
This theorem is referenced by:  eqssi  3137  eqssd  3138  sseq1  3141  sseq2  3142  eqimss  3172  dfpss3  3204  uneqin  3362  ss0b  3426  vss  3433  pssdifn0  3457  pwpw0  3704  sssn  3713  ssunsn  3715  pwsnALT  3763  unidif  3800  ssunieq  3801  uniintsn  3840  iuneq1  3859  iuneq2  3862  iunxdif2  3891  ssext  4166  pweqb  4168  eqopab2b  4231  pwun  4239  soeq2  4271  ordtri4  4366  oneqmini  4380  iunpw  4507  orduniorsuc  4558  tfi  4581  eqrel  4730  eqrelrel  4741  coeq1  4794  coeq2  4795  cnveq  4808  dmeq  4832  relssres  4945  xp11  5064  ssrnres  5069  fnres  5263  eqfnfv3  5523  fneqeql2  5533  dff3  5572  fconst4  5635  f1imaeq  5688  eqoprab2b  5805  fo1stres  6042  fo2ndres  6043  tz7.49  6390  oawordeulem  6485  nnacan  6559  nnmcan  6565  ixpeq2  6763  sbthlem3  6906  isinf  7009  ordunifi  7040  inficl  7111  rankr1c  7426  rankc1  7475  iscard  7541  iscard2  7542  carden2  7553  aleph11  7644  cardaleph  7649  alephinit  7655  dfac12a  7707  cflm  7809  cfslb2n  7827  dfacfin7  7958  wrdeq  11354  isumltss  12234  rpnnen2  12431  isprm2  12693  mrcidb2  13447  iscyggen2  15095  iscyg3  15100  lssle0  15634  islpir2  15930  iscss2  16513  ishil2  16546  bastop1  16658  epttop  16673  iscld4  16729  0ntr  16735  opnneiid  16790  isperf2  16810  cnntr  16931  ist1-3  17004  perfcls  17020  cmpfi  17062  iscon2  17067  dfcon2  17072  snfil  17486  filcon  17505  ufileu  17541  alexsubALTlem4  17671  metequiv  17982  shlesb1i  21890  shle0  21946  orthin  21950  chcon2i  21968  chcon3i  21970  chlejb1i  21980  chabs2  22021  h1datomi  22085  cmbr4i  22123  osumcor2i  22166  pjjsi  22222  pjin2i  22698  stcltr2i  22780  mdbr2  22801  dmdbr2  22808  mdsl2i  22827  mdsl2bi  22828  mdslmd3i  22837  chrelat4i  22878  sumdmdlem2  22924  dmdbr5ati  22927  dfon2lem9  23481  wfrlem8  23597  idsset  23771  domfldrefc  24388  ranfldrefc  24389  domintrefb  24394  twsymr  24409  sssu  24473  inposet  24610  dfps2  24621  hdrmp  25038  fneval  25619  equivtotbnd  25834  heiborlem10  25876  isnacs2  26113  mrefg3  26115  pmap11  29081  dia11N  30368  dia2dimlem5  30388  dib11N  30480  dih11  30585  dihglblem6  30660  doch11  30693  mapd11  30959  mapdcnv11N  30979
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-in 3101  df-ss 3108
  Copyright terms: Public domain W3C validator