Theorem eqss 3932

Description: The subclass relationship is antisymmetric. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 21-May-1993.)

Assertion

Ref	Expression
eqss	⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Proof of Theorem eqss

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		albiim 1893	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2731	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfss2 3903	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3903	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 626	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 302	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537   = wceq 1539   ∈ wcel 2108   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  eqssi  3933  eqssd  3934  sssseq  3935  sseq1  3942  sseq2  3943  eqimss  3973  ssrabeq  4013  dfpss3  4017  compleq  4078  uneqin  4209  rcompleq  4226  pssdifn0  4296  ss0b  4328  vss  4374  pwpw0  4743  sssn  4756  ssunsn  4758  pwsnOLD  4829  unidif  4872  ssunieq  4873  uniintsn  4915  iuneq1  4937  iuneq2  4940  iunxdif2  4979  ssext  5364  pweqb  5366  eqopab2bw  5454  eqopab2b  5458  pwun  5478  soeq2  5516  eqrel  5684  eqrelrel  5696  coeq1  5755  coeq2  5756  cnveq  5771  dmeq  5801  relssres  5921  xp11  6067  ssrnres  6070  ordtri4  6288  oneqmini  6302  fnres  6543  eqfnfv3  6893  fneqeql2  6906  dff3  6958  fconst4  7072  f1imaeq  7119  eqoprab2bw  7323  eqoprab2b  7324  iunpw  7599  orduniorsuc  7652  tfi  7675  fo1stres  7830  fo2ndres  7831  wfrlem8OLD  8118  tz7.49  8246  oawordeulem  8347  nnacan  8421  nnmcan  8427  ixpeq2  8657  sbthlem3  8825  isinf  8965  ordunifi  8994  inficl  9114  rankr1c  9510  rankc1  9559  iscard  9664  iscard2  9665  carden2  9676  aleph11  9771  cardaleph  9776  alephinit  9782  dfac12a  9835  cflm  9937  cfslb2n  9955  dfacfin7  10086  wrdeq  14167  isumltss  15488  rpnnen2lem12  15862  isprm2  16315  mrcidb2  17244  smndex2dnrinv  18469  iscyggen2  19396  iscyg3  19401  lssle0  20126  islpir2  20435  iscss2  20803  ishil2  20836  bastop1  22051  epttop  22067  iscld4  22124  0ntr  22130  opnneiid  22185  isperf2  22211  cnntr  22334  ist1-3  22408  perfcls  22424  cmpfi  22467  isconn2  22473  dfconn2  22478  snfil  22923  filconn  22942  ufileu  22978  alexsubALTlem4  23109  metequiv  23571  nbuhgr2vtx1edgblem  27621  iscplgr  27685  shlesb1i  29649  shle0  29705  orthin  29709  chcon2i  29727  chcon3i  29729  chlejb1i  29739  chabs2  29780  h1datomi  29844  cmbr4i  29864  osumcor2i  29907  pjjsi  29963  pjin2i  30456  stcltr2i  30538  mdbr2  30559  dmdbr2  30566  mdsl2i  30585  mdsl2bi  30586  mdslmd3i  30595  chrelat4i  30636  sumdmdlem2  30682  dmdbr5ati  30685  eqdif  30767  eqrelrd2  30857  dfon2lem9  33673  eqscut2  33927  idsset  34119  fneval  34468  topdifinfeq  35448  equivtotbnd  35863  heiborlem10  35905  eqrel2  36362  relcnveq3  36383  relcnveq2  36385  cossssid  36512  elrelscnveq3  36536  elrelscnveq2  36538  pmap11  37703  dia11N  38989  dia2dimlem5  39009  dib11N  39101  dih11  39206  dihglblem6  39281  doch11  39314  mapd11  39580  mapdcnv11N  39600  sticksstones11  40040  isnacs2  40444  mrefg3  40446  ontric3g  41027  rababg  41070  relnonrel  41084  uneqsn  41522  ntrk1k3eqk13  41549  ntrneineine1lem  41583  ntrneicls00  41588  ntrneixb  41594  ntrneik13  41597  ntrneix13  41598  joindm2  46150  meetdm2  46152