Theorem eqss 3949

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 1922	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2755	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		df-ss 3919	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3919	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 640	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 306	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570   ∈ wcel 2145   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919

This theorem is used by:  eqssi  3950  eqssd  3951  sssseq  3952  sseq1  3959  sseq2  3960  ssrabeq  4035  dfpss3  4040  compleq  4102  uneqin  4238  rcompleq  4254  pssdifn0  4319  ss0b  4354  vss  4361  pwpw0  4777  sssn  4790  ssunsn  4792  unidif  4906  ssunieq  4907  uniintsn  4948  iuneq1  4971  iuneq2  4974  iunxdif2  5016  ssext  5433  pweqb  5435  eqopab2bw  5531  eqopab2b  5535  pwun  5552  soeq2  5589  eqrel  5768  eqrelrel  5781  coeq1  5841  coeq2  5842  cnveq  5857  dmeq  5891  relssres  6019  xp11  6172  ssrnres  6175  ordtri4  6399  oneqmini  6415  fnres  6663  eqfnfv3  7028  fneqeql2  7043  dff3  7097  fconst4  7217  f1imaeq  7266  eqoprab2bw  7487  eqoprab2b  7488  iunpw  7774  orduniorsuc  7830  tfi  7853  fo1stres  8016  fo2ndres  8017  tz7.49  8438  oawordeulem  8545  nnacan  8620  nnmcan  8626  ixpeq2  8922  sbthlem3  9091  isinf  9239  ordunifi  9264  inficl  9399  rankr1c  9807  rankc1  9856  iscard  9984  iscard2  9985  carden2  9996  aleph11  10091  cardaleph  10096  alephinit  10102  dfac12a  10155  cflm  10255  cfslb2n  10274  dfacfin7  10405  wrdeq  14605  isumltss  15941  rpnnen2lem12  16319  isprm2  16778  mrcidb2  17712  smndex2dnrinv  19033  iscyggen2  20014  iscyg3  20019  lssle0  21140  islpir2  21567  iscss2  21905  ishil2  21938  bastop1  23224  epttop  23240  iscld4  23296  0ntr  23302  opnneiid  23357  isperf2  23383  cnntr  23506  ist1-3  23580  perfcls  23596  cmpfi  23639  isconn2  23645  dfconn2  23650  snfil  24096  filconn  24115  ufileu  24151  alexsubALTlem4  24282  metequiv  24741  eqcuts2  28059  nbuhgr2vtx1edgblem  29819  iscplgr  29883  shlesb1i  31875  shle0  31931  orthin  31935  chcon2i  31953  chcon3i  31955  chlejb1i  31965  chabs2  32006  h1datomi  32070  cmbr4i  32090  osumcor2i  32133  pjjsi  32189  pjin2i  32682  stcltr2i  32764  mdbr2  32785  dmdbr2  32792  mdsl2i  32811  mdsl2bi  32812  mdslmd3i  32821  chrelat4i  32862  sumdmdlem2  32908  dmdbr5ati  32911  eqdif  33002  eqrelrd2  33097  rspsnasso  33829  fnfvintima  35599  dfon2lem9  36376  idsset  36475  fneval  36979  topdifinfeq  38112  equivtotbnd  38536  heiborlem10  38578  eqrel2  39061  relcnveq3  39083  relcnveq2  39085  cossssid  39313  elrelscnveq3  39383  elrelscnveq2  39385  pmap11  40643  dia11N  41929  dia2dimlem5  41949  dib11N  42041  dih11  42146  dihglblem6  42221  doch11  42254  mapd11  42520  mapdcnv11N  42540  sticksstones11  43030  isnacs2  43559  mrefg3  43561  onsupneqmaxlim0  44073  onsupnmax  44077  ontric3g  44370  rababg  44422  relnonrel  44435  uneqsn  44873  ntrk1k3eqk13  44898  ntrneineine1lem  44932  ntrneicls00  44937  ntrneixb  44943  ntrneik13  44946  ntrneix13  44947  joindm2  49902  meetdm2  49904