Theorem eqss 3998

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1540   = wceq 1542   ∈ wcel 2107   ⊆ wss 3949

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  eqssi  3999  eqssd  4000  sssseq  4001  sseq1  4008  sseq2  4009  ssrabeq  4083  dfpss3  4087  compleq  4148  uneqin  4279  rcompleq  4296  pssdifn0  4366  ss0b  4398  vss  4444  pwpw0  4817  sssn  4830  ssunsn  4832  pwsnOLD  4902  unidif  4947  ssunieq  4948  uniintsn  4992  iuneq1  5014  iuneq2  5017  iunxdif2  5057  ssext  5455  pweqb  5457  eqopab2bw  5549  eqopab2b  5553  pwun  5573  soeq2  5611  eqrel  5785  eqrelrel  5798  coeq1  5858  coeq2  5859  cnveq  5874  dmeq  5904  relssres  6023  xp11  6175  ssrnres  6178  ordtri4  6402  oneqmini  6417  fnres  6678  eqfnfv3  7035  fneqeql2  7049  dff3  7102  fconst4  7216  f1imaeq  7264  eqoprab2bw  7479  eqoprab2b  7480  iunpw  7758  orduniorsuc  7818  tfi  7842  fo1stres  8001  fo2ndres  8002  wfrlem8OLD  8316  tz7.49  8445  oawordeulem  8554  nnacan  8628  nnmcan  8634  ixpeq2  8905  sbthlem3  9085  isinf  9260  isinfOLD  9261  ordunifi  9293  inficl  9420  rankr1c  9816  rankc1  9865  iscard  9970  iscard2  9971  carden2  9982  aleph11  10079  cardaleph  10084  alephinit  10090  dfac12a  10143  cflm  10245  cfslb2n  10263  dfacfin7  10394  wrdeq  14486  isumltss  15794  rpnnen2lem12  16168  isprm2  16619  mrcidb2  17562  smndex2dnrinv  18796  iscyggen2  19749  iscyg3  19754  lssle0  20560  islpir2  20889  iscss2  21239  ishil2  21274  bastop1  22496  epttop  22512  iscld4  22569  0ntr  22575  opnneiid  22630  isperf2  22656  cnntr  22779  ist1-3  22853  perfcls  22869  cmpfi  22912  isconn2  22918  dfconn2  22923  snfil  23368  filconn  23387  ufileu  23423  alexsubALTlem4  23554  metequiv  24018  eqscut2  27307  nbuhgr2vtx1edgblem  28608  iscplgr  28672  shlesb1i  30639  shle0  30695  orthin  30699  chcon2i  30717  chcon3i  30719  chlejb1i  30729  chabs2  30770  h1datomi  30834  cmbr4i  30854  osumcor2i  30897  pjjsi  30953  pjin2i  31446  stcltr2i  31528  mdbr2  31549  dmdbr2  31556  mdsl2i  31575  mdsl2bi  31576  mdslmd3i  31585  chrelat4i  31626  sumdmdlem2  31672  dmdbr5ati  31675  eqdif  31757  eqrelrd2  31845  rspsnasso  32492  dfon2lem9  34763  idsset  34862  fneval  35237  topdifinfeq  36231  equivtotbnd  36646  heiborlem10  36688  eqrel2  37168  relcnveq3  37190  relcnveq2  37192  cossssid  37337  elrelscnveq3  37361  elrelscnveq2  37363  pmap11  38633  dia11N  39919  dia2dimlem5  39939  dib11N  40031  dih11  40136  dihglblem6  40211  doch11  40244  mapd11  40510  mapdcnv11N  40530  sticksstones11  40972  isnacs2  41444  mrefg3  41446  onsupneqmaxlim0  41973  onsupnmax  41977  ontric3g  42273  rababg  42325  relnonrel  42338  uneqsn  42776  ntrk1k3eqk13  42801  ntrneineine1lem  42835  ntrneicls00  42840  ntrneixb  42846  ntrneik13  42849  ntrneix13  42850  joindm2  47601  meetdm2  47603