Theorem eqss 3999

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2108   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eqssi  4000  eqssd  4001  sssseq  4002  sseq1  4009  sseq2  4010  ssrabeq  4084  dfpss3  4089  compleq  4152  uneqin  4289  rcompleq  4305  pssdifn0  4368  ss0b  4401  vss  4446  pwpw0  4813  sssn  4826  ssunsn  4828  unidif  4942  ssunieq  4943  uniintsn  4985  iuneq1  5008  iuneq2  5011  iunxdif2  5053  ssext  5459  pweqb  5461  eqopab2bw  5553  eqopab2b  5557  pwun  5576  soeq2  5614  eqrel  5794  eqrelrel  5807  coeq1  5868  coeq2  5869  cnveq  5884  dmeq  5914  relssres  6040  xp11  6195  ssrnres  6198  ordtri4  6421  oneqmini  6436  fnres  6695  eqfnfv3  7053  fneqeql2  7067  dff3  7120  fconst4  7234  f1imaeq  7285  eqoprab2bw  7503  eqoprab2b  7504  iunpw  7791  orduniorsuc  7850  tfi  7874  fo1stres  8040  fo2ndres  8041  wfrlem8OLD  8356  tz7.49  8485  oawordeulem  8592  nnacan  8666  nnmcan  8672  ixpeq2  8951  sbthlem3  9125  isinf  9296  isinfOLD  9297  ordunifi  9326  inficl  9465  rankr1c  9861  rankc1  9910  iscard  10015  iscard2  10016  carden2  10027  aleph11  10124  cardaleph  10129  alephinit  10135  dfac12a  10189  cflm  10290  cfslb2n  10308  dfacfin7  10439  wrdeq  14574  isumltss  15884  rpnnen2lem12  16261  isprm2  16719  mrcidb2  17661  smndex2dnrinv  18928  iscyggen2  19899  iscyg3  19904  lssle0  20948  islpir2  21340  iscss2  21704  ishil2  21739  bastop1  23000  epttop  23016  iscld4  23073  0ntr  23079  opnneiid  23134  isperf2  23160  cnntr  23283  ist1-3  23357  perfcls  23373  cmpfi  23416  isconn2  23422  dfconn2  23427  snfil  23872  filconn  23891  ufileu  23927  alexsubALTlem4  24058  metequiv  24522  eqscut2  27851  nbuhgr2vtx1edgblem  29368  iscplgr  29432  shlesb1i  31405  shle0  31461  orthin  31465  chcon2i  31483  chcon3i  31485  chlejb1i  31495  chabs2  31536  h1datomi  31600  cmbr4i  31620  osumcor2i  31663  pjjsi  31719  pjin2i  32212  stcltr2i  32294  mdbr2  32315  dmdbr2  32322  mdsl2i  32341  mdsl2bi  32342  mdslmd3i  32351  chrelat4i  32392  sumdmdlem2  32438  dmdbr5ati  32441  eqdif  32538  eqrelrd2  32628  rspsnasso  33416  dfon2lem9  35792  idsset  35891  fneval  36353  topdifinfeq  37351  equivtotbnd  37785  heiborlem10  37827  eqrel2  38300  relcnveq3  38322  relcnveq2  38324  cossssid  38468  elrelscnveq3  38492  elrelscnveq2  38494  pmap11  39764  dia11N  41050  dia2dimlem5  41070  dib11N  41162  dih11  41267  dihglblem6  41342  doch11  41375  mapd11  41641  mapdcnv11N  41661  sticksstones11  42157  isnacs2  42717  mrefg3  42719  onsupneqmaxlim0  43236  onsupnmax  43240  ontric3g  43535  rababg  43587  relnonrel  43600  uneqsn  44038  ntrk1k3eqk13  44063  ntrneineine1lem  44097  ntrneicls00  44102  ntrneixb  44108  ntrneik13  44111  ntrneix13  44112  joindm2  48865  meetdm2  48867