Theorem eqss 3984

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 1890	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2817	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfss2 3957	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3957	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 628	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 305	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535   = wceq 1537   ∈ wcel 2114   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954

This theorem is referenced by:  eqssi  3985  eqssd  3986  sssseq  3987  sseq1  3994  sseq2  3995  eqimss  4025  ssrabeq  4061  dfpss3  4065  compleq  4126  uneqin  4257  pssdifn0  4327  ss0b  4353  vss  4397  pwpw0  4748  sssn  4761  ssunsn  4763  pwsnOLD  4833  unidif  4874  ssunieq  4875  uniintsn  4915  iuneq1  4937  iuneq2  4940  iunxdif2  4979  ssext  5349  pweqb  5351  eqopab2bw  5437  eqopab2b  5441  pwun  5460  soeq2  5497  eqrel  5660  eqrelrel  5672  coeq1  5730  coeq2  5731  cnveq  5746  dmeq  5774  relssres  5895  xp11  6034  ssrnres  6037  ordtri4  6230  oneqmini  6244  fnres  6476  eqfnfv3  6806  fneqeql2  6819  dff3  6868  fconst4  6979  f1imaeq  7025  eqoprab2bw  7226  eqoprab2b  7227  iunpw  7495  orduniorsuc  7547  tfi  7570  fo1stres  7717  fo2ndres  7718  wfrlem8  7964  tz7.49  8083  oawordeulem  8182  nnacan  8256  nnmcan  8262  ixpeq2  8477  sbthlem3  8631  isinf  8733  ordunifi  8770  inficl  8891  rankr1c  9252  rankc1  9301  iscard  9406  iscard2  9407  carden2  9418  aleph11  9512  cardaleph  9517  alephinit  9523  dfac12a  9576  cflm  9674  cfslb2n  9692  dfacfin7  9823  wrdeq  13888  isumltss  15205  rpnnen2lem12  15580  isprm2  16028  mrcidb2  16891  smndex2dnrinv  18082  iscyggen2  19002  iscyg3  19007  lssle0  19723  islpir2  20026  iscss2  20832  ishil2  20865  bastop1  21603  epttop  21619  iscld4  21675  0ntr  21681  opnneiid  21736  isperf2  21762  cnntr  21885  ist1-3  21959  perfcls  21975  cmpfi  22018  isconn2  22024  dfconn2  22029  snfil  22474  filconn  22493  ufileu  22529  alexsubALTlem4  22660  metequiv  23121  nbuhgr2vtx1edgblem  27135  iscplgr  27199  shlesb1i  29165  shle0  29221  orthin  29225  chcon2i  29243  chcon3i  29245  chlejb1i  29255  chabs2  29296  h1datomi  29360  cmbr4i  29380  osumcor2i  29423  pjjsi  29479  pjin2i  29972  stcltr2i  30054  mdbr2  30075  dmdbr2  30082  mdsl2i  30101  mdsl2bi  30102  mdslmd3i  30111  chrelat4i  30152  sumdmdlem2  30198  dmdbr5ati  30201  eqdif  30283  eqrelrd2  30369  dfon2lem9  33038  idsset  33353  fneval  33702  topdifinfeq  34633  equivtotbnd  35058  heiborlem10  35100  eqrel2  35559  relcnveq3  35580  relcnveq2  35582  cossssid  35709  elrelscnveq3  35733  elrelscnveq2  35735  pmap11  36900  dia11N  38186  dia2dimlem5  38206  dib11N  38298  dih11  38403  dihglblem6  38478  doch11  38511  mapd11  38777  mapdcnv11N  38797  isnacs2  39310  mrefg3  39312  ontric3g  39895  rababg  39940  relnonrel  39954  rcompleq  40377  uneqsn  40380  ntrk1k3eqk13  40407  ntrneineine1lem  40441  ntrneicls00  40446  ntrneixb  40452  ntrneik13  40455  ntrneix13  40456