Theorem eqss 3618

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 1816	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2616	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfss2 3591	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3591	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 733	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 292	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1481   = wceq 1483   ∈ wcel 1990   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  eqssi  3619  eqssd  3620  sssseq  3621  sseq1  3626  sseq2  3627  eqimss  3657  ssrabeq  3689  dfpss3  3693  compleq  3752  uneqin  3878  pssdifn0  3944  ss0b  3973  vss  4012  pwpw0  4344  sssn  4358  ssunsn  4360  pwsnALT  4429  unidif  4471  ssunieq  4472  uniintsn  4514  iuneq1  4534  iuneq2  4537  iunxdif2  4568  ssext  4923  pweqb  4925  eqopab2b  5005  pwun  5022  soeq2  5055  eqrel  5209  eqrelrel  5221  coeq1  5279  coeq2  5280  cnveq  5296  dmeq  5324  relssres  5437  xp11  5569  ssrnres  5572  ordtri4  5761  oneqmini  5776  fnres  6007  eqfnfv3  6313  fneqeql2  6326  dff3  6372  fconst4  6478  f1imaeq  6522  eqoprab2b  6713  iunpw  6978  orduniorsuc  7030  tfi  7053  fo1stres  7192  fo2ndres  7193  wfrlem8  7422  tz7.49  7540  oawordeulem  7634  nnacan  7708  nnmcan  7714  ixpeq2  7922  sbthlem3  8072  isinf  8173  ordunifi  8210  inficl  8331  rankr1c  8684  rankc1  8733  iscard  8801  iscard2  8802  carden2  8813  aleph11  8907  cardaleph  8912  alephinit  8918  dfac12a  8970  cflm  9072  cfslb2n  9090  dfacfin7  9221  wrdeq  13327  isumltss  14580  rpnnen2lem12  14954  isprm2  15395  mrcidb2  16278  iscyggen2  18283  iscyg3  18288  lssle0  18950  islpir2  19251  iscss2  20030  ishil2  20063  bastop1  20797  epttop  20813  iscld4  20869  0ntr  20875  opnneiid  20930  isperf2  20956  cnntr  21079  ist1-3  21153  perfcls  21169  cmpfi  21211  isconn2  21217  dfconn2  21222  snfil  21668  filconn  21687  ufileu  21723  alexsubALTlem4  21854  metequiv  22314  nbuhgr2vtx1edgblem  26247  shlesb1i  28245  shle0  28301  orthin  28305  chcon2i  28323  chcon3i  28325  chlejb1i  28335  chabs2  28376  h1datomi  28440  cmbr4i  28460  osumcor2i  28503  pjjsi  28559  pjin2i  29052  stcltr2i  29134  mdbr2  29155  dmdbr2  29162  mdsl2i  29181  mdsl2bi  29182  mdslmd3i  29191  chrelat4i  29232  sumdmdlem2  29278  dmdbr5ati  29281  eqrelrd2  29426  dfon2lem9  31696  idsset  31997  fneval  32347  topdifinfeq  33198  equivtotbnd  33577  heiborlem10  33619  eqrel2  34068  relcnveq3  34092  relcnveq2  34094  pmap11  35048  dia11N  36337  dia2dimlem5  36357  dib11N  36449  dih11  36554  dihglblem6  36629  doch11  36662  mapd11  36928  mapdcnv11N  36948  isnacs2  37269  mrefg3  37271  rababg  37879  relnonrel  37893  rcompleq  38318  uneqsn  38321  ntrk1k3eqk13  38348  ntrneineine1lem  38382  ntrneicls00  38387  ntrneixb  38393  ntrneik13  38396  ntrneix13  38397  prsal  40538