Theorem eqss 3928

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 1924	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2756	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		df-ss 3901	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3901	. . 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 2147   ⊆ wss 3900

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eqssi  3929  eqssd  3930  sssseq  3931  sseq1  3938  sseq2  3939  ssrabeq  4012  dfpss3  4019  compleq  4091  uneqin  4237  rcompleq  4253  pssdifn0  4319  ss0b  4354  vss  4361  sssn  4785  ssunsn  4787  pwpw0  4834  unidif  4906  ssunieq  4907  uniintsn  4948  iuneq1  4971  iuneq2  4974  iunxdif2  5015  ssext  5427  pweqb  5429  eqopab2bw  5528  eqopab2b  5532  pwun  5549  soeq2  5586  eqrel  5766  eqrelrel  5779  coeq1  5842  coeq2  5843  cnveq  5859  dmeq  5893  relssres  6024  xp11  6180  ssrnres  6183  cnveqb  6203  ordtri4  6421  oneqmini  6437  fnres  6691  eqfnfv3  7057  fneqeql2  7072  dff3  7127  fconst4  7246  f1imaeq  7295  eqoprab2bw  7516  eqoprab2b  7517  iunpw  7812  orduniorsuc  7868  tfi  7891  fo1stres  8054  fo2ndres  8055  tz7.49  8486  oawordeulem  8593  nnacan  8668  nnmcan  8674  ixpeq2  8970  sbthlem3  9139  isinf  9287  ordunifi  9312  inficl  9447  rankr1c  9860  rankc1  9917  iscard  10086  iscard2  10087  carden2  10098  aleph11  10193  cardaleph  10198  alephinit  10204  dfac12a  10257  cflm  10357  cfslb2n  10376  dfacfin7  10507  wrdeq  14711  isumltss  16049  rpnnen2lem12  16425  isprm2  16889  mrcidb2  17824  smndex2dnrinv  19146  iscyggen2  20128  iscyg3  20133  lssle0  21258  islpir2  21687  iscss2  22025  ishil2  22058  bastop1  23344  epttop  23360  iscld4  23416  0ntr  23422  opnneiid  23477  isperf2  23503  cnntr  23626  ist1-3  23700  perfcls  23716  cmpfi  23759  isconn2  23765  dfconn2  23770  snfil  24216  filconn  24235  ufileu  24271  alexsubALTlem4  24402  metequiv  24861  eqcuts2  28205  nbuhgr2vtx1edgblem  29965  iscplgr  30029  shlesb1i  32021  shle0  32077  orthin  32081  chcon2i  32099  chcon3i  32101  chlejb1i  32111  chabs2  32152  h1datomi  32216  cmbr4i  32236  osumcor2i  32279  pjjsi  32335  pjin2i  32828  stcltr2i  32910  mdbr2  32931  dmdbr2  32938  mdsl2i  32957  mdsl2bi  32958  mdslmd3i  32967  chrelat4i  33008  sumdmdlem2  33054  dmdbr5ati  33057  eqdif  33190  eqrelrd2  33285  rspsnasso  34027  fnfvintima  35799  dfon2lem9  36744  idsset  36843  fneval  37331  topdifinfeq  38478  equivtotbnd  38915  heiborlem10  38957  eqrel2  39440  relcnveq3  39462  relcnveq2  39464  cossssid  39692  elrelscnveq3  39762  elrelscnveq2  39764  pmap11  41022  dia11N  42308  dia2dimlem5  42328  dib11N  42420  dih11  42525  dihglblem6  42600  doch11  42633  mapd11  42899  mapdcnv11N  42919  sticksstones11  43409  isnacs2  43921  mrefg3  43923  onsupneqmaxlim0  44429  onsupnmax  44433  ontric3g  44726  rababg  44778  relnonrel  44790  uneqsn  45228  ntrk1k3eqk13  45253  ntrneineine1lem  45287  ntrneicls00  45292  ntrneixb  45298  ntrneik13  45301  ntrneix13  45302  cocan2g  46126  cocan1g  46128  joindm2  50297  meetdm2  50299