Theorem eqss 3997

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 3968	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3968	. . 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 3948

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 3955  df-ss 3965

This theorem is referenced by:  eqssi  3998  eqssd  3999  sssseq  4000  sseq1  4007  sseq2  4008  ssrabeq  4082  dfpss3  4086  compleq  4147  uneqin  4278  rcompleq  4295  pssdifn0  4365  ss0b  4397  vss  4443  pwpw0  4816  sssn  4829  ssunsn  4831  pwsnOLD  4901  unidif  4946  ssunieq  4947  uniintsn  4991  iuneq1  5013  iuneq2  5016  iunxdif2  5056  ssext  5454  pweqb  5456  eqopab2bw  5548  eqopab2b  5552  pwun  5572  soeq2  5610  eqrel  5783  eqrelrel  5796  coeq1  5856  coeq2  5857  cnveq  5872  dmeq  5902  relssres  6021  xp11  6172  ssrnres  6175  ordtri4  6399  oneqmini  6414  fnres  6675  eqfnfv3  7032  fneqeql2  7046  dff3  7099  fconst4  7213  f1imaeq  7261  eqoprab2bw  7476  eqoprab2b  7477  iunpw  7755  orduniorsuc  7815  tfi  7839  fo1stres  7998  fo2ndres  7999  wfrlem8OLD  8313  tz7.49  8442  oawordeulem  8551  nnacan  8625  nnmcan  8631  ixpeq2  8902  sbthlem3  9082  isinf  9257  isinfOLD  9258  ordunifi  9290  inficl  9417  rankr1c  9813  rankc1  9862  iscard  9967  iscard2  9968  carden2  9979  aleph11  10076  cardaleph  10081  alephinit  10087  dfac12a  10140  cflm  10242  cfslb2n  10260  dfacfin7  10391  wrdeq  14483  isumltss  15791  rpnnen2lem12  16165  isprm2  16616  mrcidb2  17559  smndex2dnrinv  18793  iscyggen2  19744  iscyg3  19749  lssle0  20553  islpir2  20882  iscss2  21231  ishil2  21266  bastop1  22488  epttop  22504  iscld4  22561  0ntr  22567  opnneiid  22622  isperf2  22648  cnntr  22771  ist1-3  22845  perfcls  22861  cmpfi  22904  isconn2  22910  dfconn2  22915  snfil  23360  filconn  23379  ufileu  23415  alexsubALTlem4  23546  metequiv  24010  eqscut2  27297  nbuhgr2vtx1edgblem  28598  iscplgr  28662  shlesb1i  30627  shle0  30683  orthin  30687  chcon2i  30705  chcon3i  30707  chlejb1i  30717  chabs2  30758  h1datomi  30822  cmbr4i  30842  osumcor2i  30885  pjjsi  30941  pjin2i  31434  stcltr2i  31516  mdbr2  31537  dmdbr2  31544  mdsl2i  31563  mdsl2bi  31564  mdslmd3i  31573  chrelat4i  31614  sumdmdlem2  31660  dmdbr5ati  31663  eqdif  31745  eqrelrd2  31833  rspsnasso  32481  dfon2lem9  34752  idsset  34851  fneval  35226  topdifinfeq  36220  equivtotbnd  36635  heiborlem10  36677  eqrel2  37157  relcnveq3  37179  relcnveq2  37181  cossssid  37326  elrelscnveq3  37350  elrelscnveq2  37352  pmap11  38622  dia11N  39908  dia2dimlem5  39928  dib11N  40020  dih11  40125  dihglblem6  40200  doch11  40233  mapd11  40499  mapdcnv11N  40519  sticksstones11  40961  isnacs2  41430  mrefg3  41432  onsupneqmaxlim0  41959  onsupnmax  41963  ontric3g  42259  rababg  42311  relnonrel  42324  uneqsn  42762  ntrk1k3eqk13  42787  ntrneineine1lem  42821  ntrneicls00  42826  ntrneixb  42832  ntrneik13  42835  ntrneix13  42836  joindm2  47555  meetdm2  47557