Theorem eqss 3953

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568   = wceq 1570   ∈ wcel 2143   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  eqssi  3954  eqssd  3955  sssseq  3956  sseq1  3963  sseq2  3964  ssrabeq  4039  dfpss3  4044  compleq  4107  uneqin  4243  rcompleq  4259  pssdifn0  4324  ss0b  4359  vss  4366  pwpw0  4780  sssn  4793  ssunsn  4795  unidif  4909  ssunieq  4910  uniintsn  4951  iuneq1  4974  iuneq2  4977  iunxdif2  5019  ssext  5437  pweqb  5439  eqopab2bw  5535  eqopab2b  5539  pwun  5556  soeq2  5593  eqrel  5772  eqrelrel  5785  coeq1  5845  coeq2  5846  cnveq  5861  dmeq  5895  relssres  6023  xp11  6175  ssrnres  6178  ordtri4  6400  oneqmini  6416  fnres  6664  eqfnfv3  7029  fneqeql2  7044  dff3  7097  fconst4  7214  f1imaeq  7265  eqoprab2bw  7482  eqoprab2b  7483  iunpw  7771  orduniorsuc  7827  tfi  7850  fo1stres  8013  fo2ndres  8014  tz7.49  8433  oawordeulem  8540  nnacan  8615  nnmcan  8621  ixpeq2  8910  sbthlem3  9078  isinf  9226  ordunifi  9251  inficl  9386  rankr1c  9794  rankc1  9843  iscard  9962  iscard2  9963  carden2  9974  aleph11  10069  cardaleph  10074  alephinit  10080  dfac12a  10133  cflm  10234  cfslb2n  10253  dfacfin7  10384  wrdeq  14575  isumltss  15904  rpnnen2lem12  16282  isprm2  16741  mrcidb2  17675  smndex2dnrinv  18978  iscyggen2  19952  iscyg3  19957  lssle0  21052  islpir2  21479  iscss2  21817  ishil2  21850  bastop1  23131  epttop  23147  iscld4  23203  0ntr  23209  opnneiid  23264  isperf2  23290  cnntr  23413  ist1-3  23487  perfcls  23503  cmpfi  23546  isconn2  23552  dfconn2  23557  snfil  24002  filconn  24021  ufileu  24057  alexsubALTlem4  24188  metequiv  24647  eqcuts2  27960  nbuhgr2vtx1edgblem  29682  iscplgr  29746  shlesb1i  31719  shle0  31775  orthin  31779  chcon2i  31797  chcon3i  31799  chlejb1i  31809  chabs2  31850  h1datomi  31914  cmbr4i  31934  osumcor2i  31977  pjjsi  32033  pjin2i  32526  stcltr2i  32608  mdbr2  32629  dmdbr2  32636  mdsl2i  32655  mdsl2bi  32656  mdslmd3i  32665  chrelat4i  32706  sumdmdlem2  32752  dmdbr5ati  32755  eqdif  32846  eqrelrd2  32942  rspsnasso  33682  fnfvintima  35457  dfon2lem9  36262  idsset  36361  fneval  36844  topdifinfeq  37977  equivtotbnd  38410  heiborlem10  38452  eqrel2  38935  relcnveq3  38957  relcnveq2  38959  cossssid  39187  elrelscnveq3  39257  elrelscnveq2  39259  pmap11  40517  dia11N  41803  dia2dimlem5  41823  dib11N  41915  dih11  42020  dihglblem6  42095  doch11  42128  mapd11  42394  mapdcnv11N  42414  sticksstones11  42904  isnacs2  43420  mrefg3  43422  onsupneqmaxlim0  43934  onsupnmax  43938  ontric3g  44231  rababg  44283  relnonrel  44296  uneqsn  44734  ntrk1k3eqk13  44759  ntrneineine1lem  44793  ntrneicls00  44798  ntrneixb  44804  ntrneik13  44807  ntrneix13  44808  joindm2  49729  meetdm2  49731