Theorem eqss 3946

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 2726	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		df-ss 3915	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3915	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 628	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 303	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541   ∈ wcel 2113   ⊆ wss 3898

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 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  eqssi  3947  eqssd  3948  sssseq  3949  sseq1  3956  sseq2  3957  ssrabeq  4033  dfpss3  4038  compleq  4101  uneqin  4238  rcompleq  4254  pssdifn0  4317  ss0b  4350  vss  4395  pwpw0  4764  sssn  4777  ssunsn  4779  unidif  4893  ssunieq  4894  uniintsn  4935  iuneq1  4958  iuneq2  4961  iunxdif2  5004  ssext  5397  pweqb  5399  eqopab2bw  5491  eqopab2b  5495  pwun  5512  soeq2  5549  eqrel  5728  eqrelrel  5741  coeq1  5801  coeq2  5802  cnveq  5817  dmeq  5847  relssres  5975  xp11  6127  ssrnres  6130  ordtri4  6348  oneqmini  6364  fnres  6613  eqfnfv3  6972  fneqeql2  6986  dff3  7039  fconst4  7154  f1imaeq  7205  eqoprab2bw  7422  eqoprab2b  7423  iunpw  7710  orduniorsuc  7766  tfi  7789  fo1stres  7953  fo2ndres  7954  tz7.49  8370  oawordeulem  8475  nnacan  8549  nnmcan  8555  ixpeq2  8841  sbthlem3  9009  isinf  9156  ordunifi  9181  inficl  9316  rankr1c  9721  rankc1  9770  iscard  9875  iscard2  9876  carden2  9887  aleph11  9982  cardaleph  9987  alephinit  9993  dfac12a  10047  cflm  10148  cfslb2n  10166  dfacfin7  10297  wrdeq  14445  isumltss  15757  rpnnen2lem12  16136  isprm2  16595  mrcidb2  17526  smndex2dnrinv  18825  iscyggen2  19795  iscyg3  19800  lssle0  20885  islpir2  21269  iscss2  21625  ishil2  21658  bastop1  22909  epttop  22925  iscld4  22981  0ntr  22987  opnneiid  23042  isperf2  23068  cnntr  23191  ist1-3  23265  perfcls  23281  cmpfi  23324  isconn2  23330  dfconn2  23335  snfil  23780  filconn  23799  ufileu  23835  alexsubALTlem4  23966  metequiv  24425  eqscut2  27748  nbuhgr2vtx1edgblem  29331  iscplgr  29395  shlesb1i  31368  shle0  31424  orthin  31428  chcon2i  31446  chcon3i  31448  chlejb1i  31458  chabs2  31499  h1datomi  31563  cmbr4i  31583  osumcor2i  31626  pjjsi  31682  pjin2i  32175  stcltr2i  32257  mdbr2  32278  dmdbr2  32285  mdsl2i  32304  mdsl2bi  32305  mdslmd3i  32314  chrelat4i  32355  sumdmdlem2  32401  dmdbr5ati  32404  eqdif  32501  eqrelrd2  32601  rspsnasso  33360  dfon2lem9  35854  idsset  35953  fneval  36417  topdifinfeq  37415  equivtotbnd  37838  heiborlem10  37880  eqrel2  38357  relcnveq3  38379  relcnveq2  38381  cossssid  38589  elrelscnveq3  38659  elrelscnveq2  38661  pmap11  39881  dia11N  41167  dia2dimlem5  41187  dib11N  41279  dih11  41384  dihglblem6  41459  doch11  41492  mapd11  41758  mapdcnv11N  41778  sticksstones11  42269  isnacs2  42823  mrefg3  42825  onsupneqmaxlim0  43341  onsupnmax  43345  ontric3g  43639  rababg  43691  relnonrel  43704  uneqsn  44142  ntrk1k3eqk13  44167  ntrneineine1lem  44201  ntrneicls00  44206  ntrneixb  44212  ntrneik13  44215  ntrneix13  44216  joindm2  49092  meetdm2  49094