Theorem eqss 3951

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542   ∈ wcel 2114   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  eqssi  3952  eqssd  3953  sssseq  3954  sseq1  3961  sseq2  3962  ssrabeq  4038  dfpss3  4043  compleq  4106  uneqin  4243  rcompleq  4259  pssdifn0  4322  ss0b  4355  vss  4400  pwpw0  4771  sssn  4784  ssunsn  4786  unidif  4900  ssunieq  4901  uniintsn  4942  iuneq1  4965  iuneq2  4968  iunxdif2  5011  ssext  5409  pweqb  5411  eqopab2bw  5504  eqopab2b  5508  pwun  5525  soeq2  5562  eqrel  5741  eqrelrel  5754  coeq1  5814  coeq2  5815  cnveq  5830  dmeq  5860  relssres  5989  xp11  6141  ssrnres  6144  ordtri4  6362  oneqmini  6378  fnres  6627  eqfnfv3  6987  fneqeql2  7001  dff3  7054  fconst4  7170  f1imaeq  7221  eqoprab2bw  7438  eqoprab2b  7439  iunpw  7726  orduniorsuc  7782  tfi  7805  fo1stres  7969  fo2ndres  7970  tz7.49  8386  oawordeulem  8491  nnacan  8566  nnmcan  8572  ixpeq2  8861  sbthlem3  9029  isinf  9177  ordunifi  9202  inficl  9340  rankr1c  9745  rankc1  9794  iscard  9899  iscard2  9900  carden2  9911  aleph11  10006  cardaleph  10011  alephinit  10017  dfac12a  10071  cflm  10172  cfslb2n  10190  dfacfin7  10321  wrdeq  14471  isumltss  15783  rpnnen2lem12  16162  isprm2  16621  mrcidb2  17553  smndex2dnrinv  18852  iscyggen2  19822  iscyg3  19827  lssle0  20913  islpir2  21297  iscss2  21653  ishil2  21686  bastop1  22949  epttop  22965  iscld4  23021  0ntr  23027  opnneiid  23082  isperf2  23108  cnntr  23231  ist1-3  23305  perfcls  23321  cmpfi  23364  isconn2  23370  dfconn2  23375  snfil  23820  filconn  23839  ufileu  23875  alexsubALTlem4  24006  metequiv  24465  eqcuts2  27794  nbuhgr2vtx1edgblem  29436  iscplgr  29500  shlesb1i  31473  shle0  31529  orthin  31533  chcon2i  31551  chcon3i  31553  chlejb1i  31563  chabs2  31604  h1datomi  31668  cmbr4i  31688  osumcor2i  31731  pjjsi  31787  pjin2i  32280  stcltr2i  32362  mdbr2  32383  dmdbr2  32390  mdsl2i  32409  mdsl2bi  32410  mdslmd3i  32419  chrelat4i  32460  sumdmdlem2  32506  dmdbr5ati  32509  eqdif  32605  eqrelrd2  32705  rspsnasso  33480  dfon2lem9  36002  idsset  36101  fneval  36565  topdifinfeq  37602  equivtotbnd  38026  heiborlem10  38068  eqrel2  38553  relcnveq3  38575  relcnveq2  38577  cossssid  38805  elrelscnveq3  38875  elrelscnveq2  38877  pmap11  40135  dia11N  41421  dia2dimlem5  41441  dib11N  41533  dih11  41638  dihglblem6  41713  doch11  41746  mapd11  42012  mapdcnv11N  42032  sticksstones11  42523  isnacs2  43060  mrefg3  43062  onsupneqmaxlim0  43578  onsupnmax  43582  ontric3g  43875  rababg  43927  relnonrel  43940  uneqsn  44378  ntrk1k3eqk13  44403  ntrneineine1lem  44437  ntrneicls00  44442  ntrneixb  44448  ntrneik13  44451  ntrneix13  44452  joindm2  49324  meetdm2  49326