Theorem eqss 3946

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541   ∈ wcel 2113   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  eqssi  3947  eqssd  3948  sssseq  3949  sseq1  3956  sseq2  3957  ssrabeq  4033  dfpss3  4038  compleq  4101  uneqin  4238  rcompleq  4254  pssdifn0  4317  ss0b  4350  vss  4395  pwpw0  4766  sssn  4779  ssunsn  4781  unidif  4895  ssunieq  4896  uniintsn  4937  iuneq1  4960  iuneq2  4963  iunxdif2  5006  ssext  5399  pweqb  5401  eqopab2bw  5493  eqopab2b  5497  pwun  5514  soeq2  5551  eqrel  5730  eqrelrel  5743  coeq1  5803  coeq2  5804  cnveq  5819  dmeq  5849  relssres  5977  xp11  6129  ssrnres  6132  ordtri4  6350  oneqmini  6366  fnres  6615  eqfnfv3  6974  fneqeql2  6988  dff3  7041  fconst4  7156  f1imaeq  7207  eqoprab2bw  7424  eqoprab2b  7425  iunpw  7712  orduniorsuc  7768  tfi  7791  fo1stres  7955  fo2ndres  7956  tz7.49  8372  oawordeulem  8477  nnacan  8551  nnmcan  8557  ixpeq2  8843  sbthlem3  9011  isinf  9158  ordunifi  9183  inficl  9318  rankr1c  9723  rankc1  9772  iscard  9877  iscard2  9878  carden2  9889  aleph11  9984  cardaleph  9989  alephinit  9995  dfac12a  10049  cflm  10150  cfslb2n  10168  dfacfin7  10299  wrdeq  14447  isumltss  15759  rpnnen2lem12  16138  isprm2  16597  mrcidb2  17528  smndex2dnrinv  18827  iscyggen2  19797  iscyg3  19802  lssle0  20887  islpir2  21271  iscss2  21627  ishil2  21660  bastop1  22911  epttop  22927  iscld4  22983  0ntr  22989  opnneiid  23044  isperf2  23070  cnntr  23193  ist1-3  23267  perfcls  23283  cmpfi  23326  isconn2  23332  dfconn2  23337  snfil  23782  filconn  23801  ufileu  23837  alexsubALTlem4  23968  metequiv  24427  eqscut2  27750  nbuhgr2vtx1edgblem  29333  iscplgr  29397  shlesb1i  31370  shle0  31426  orthin  31430  chcon2i  31448  chcon3i  31450  chlejb1i  31460  chabs2  31501  h1datomi  31565  cmbr4i  31585  osumcor2i  31628  pjjsi  31684  pjin2i  32177  stcltr2i  32259  mdbr2  32280  dmdbr2  32287  mdsl2i  32306  mdsl2bi  32307  mdslmd3i  32316  chrelat4i  32357  sumdmdlem2  32403  dmdbr5ati  32406  eqdif  32503  eqrelrd2  32603  rspsnasso  33362  dfon2lem9  35856  idsset  35955  fneval  36419  topdifinfeq  37417  equivtotbnd  37841  heiborlem10  37883  eqrel2  38360  relcnveq3  38382  relcnveq2  38384  cossssid  38592  elrelscnveq3  38662  elrelscnveq2  38664  pmap11  39884  dia11N  41170  dia2dimlem5  41190  dib11N  41282  dih11  41387  dihglblem6  41462  doch11  41495  mapd11  41761  mapdcnv11N  41781  sticksstones11  42272  isnacs2  42826  mrefg3  42828  onsupneqmaxlim0  43344  onsupnmax  43348  ontric3g  43642  rababg  43694  relnonrel  43707  uneqsn  44145  ntrk1k3eqk13  44170  ntrneineine1lem  44204  ntrneicls00  44209  ntrneixb  44215  ntrneik13  44218  ntrneix13  44219  joindm2  49095  meetdm2  49097