Theorem eqss 3936

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 1892	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2731	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfss2 3907	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3907	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 627	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 303	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537   = wceq 1539   ∈ wcel 2106   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  eqssi  3937  eqssd  3938  sssseq  3939  sseq1  3946  sseq2  3947  eqimss  3977  ssrabeq  4017  dfpss3  4021  compleq  4082  uneqin  4212  rcompleq  4229  pssdifn0  4299  ss0b  4331  vss  4377  pwpw0  4746  sssn  4759  ssunsn  4761  pwsnOLD  4832  unidif  4875  ssunieq  4876  uniintsn  4918  iuneq1  4940  iuneq2  4943  iunxdif2  4983  ssext  5370  pweqb  5372  eqopab2bw  5461  eqopab2b  5465  pwun  5487  soeq2  5525  eqrel  5695  eqrelrel  5707  coeq1  5766  coeq2  5767  cnveq  5782  dmeq  5812  relssres  5932  xp11  6078  ssrnres  6081  ordtri4  6303  oneqmini  6317  fnres  6559  eqfnfv3  6911  fneqeql2  6924  dff3  6976  fconst4  7090  f1imaeq  7138  eqoprab2bw  7345  eqoprab2b  7346  iunpw  7621  orduniorsuc  7677  tfi  7700  fo1stres  7857  fo2ndres  7858  wfrlem8OLD  8147  tz7.49  8276  oawordeulem  8385  nnacan  8459  nnmcan  8465  ixpeq2  8699  sbthlem3  8872  isinf  9036  ordunifi  9064  inficl  9184  rankr1c  9579  rankc1  9628  iscard  9733  iscard2  9734  carden2  9745  aleph11  9840  cardaleph  9845  alephinit  9851  dfac12a  9904  cflm  10006  cfslb2n  10024  dfacfin7  10155  wrdeq  14239  isumltss  15560  rpnnen2lem12  15934  isprm2  16387  mrcidb2  17327  smndex2dnrinv  18554  iscyggen2  19481  iscyg3  19486  lssle0  20211  islpir2  20522  iscss2  20891  ishil2  20926  bastop1  22143  epttop  22159  iscld4  22216  0ntr  22222  opnneiid  22277  isperf2  22303  cnntr  22426  ist1-3  22500  perfcls  22516  cmpfi  22559  isconn2  22565  dfconn2  22570  snfil  23015  filconn  23034  ufileu  23070  alexsubALTlem4  23201  metequiv  23665  nbuhgr2vtx1edgblem  27718  iscplgr  27782  shlesb1i  29748  shle0  29804  orthin  29808  chcon2i  29826  chcon3i  29828  chlejb1i  29838  chabs2  29879  h1datomi  29943  cmbr4i  29963  osumcor2i  30006  pjjsi  30062  pjin2i  30555  stcltr2i  30637  mdbr2  30658  dmdbr2  30665  mdsl2i  30684  mdsl2bi  30685  mdslmd3i  30694  chrelat4i  30735  sumdmdlem2  30781  dmdbr5ati  30784  eqdif  30866  eqrelrd2  30956  dfon2lem9  33767  eqscut2  34000  idsset  34192  fneval  34541  topdifinfeq  35521  equivtotbnd  35936  heiborlem10  35978  eqrel2  36435  relcnveq3  36456  relcnveq2  36458  cossssid  36585  elrelscnveq3  36609  elrelscnveq2  36611  pmap11  37776  dia11N  39062  dia2dimlem5  39082  dib11N  39174  dih11  39279  dihglblem6  39354  doch11  39387  mapd11  39653  mapdcnv11N  39673  sticksstones11  40112  isnacs2  40528  mrefg3  40530  ontric3g  41129  rababg  41181  relnonrel  41195  uneqsn  41633  ntrk1k3eqk13  41660  ntrneineine1lem  41694  ntrneicls00  41699  ntrneixb  41705  ntrneik13  41708  ntrneix13  41709  joindm2  46262  meetdm2  46264