Theorem eqss 3979

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 2729	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		df-ss 3948	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3948	. . 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 2109   ⊆ wss 3931

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 2008  ax-9 2119  ax-ext 2708

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

This theorem is referenced by:  eqssi  3980  eqssd  3981  sssseq  3982  sseq1  3989  sseq2  3990  ssrabeq  4064  dfpss3  4069  compleq  4132  uneqin  4269  rcompleq  4285  pssdifn0  4348  ss0b  4381  vss  4426  pwpw0  4794  sssn  4807  ssunsn  4809  unidif  4923  ssunieq  4924  uniintsn  4966  iuneq1  4989  iuneq2  4992  iunxdif2  5034  ssext  5434  pweqb  5436  eqopab2bw  5528  eqopab2b  5532  pwun  5551  soeq2  5588  eqrel  5768  eqrelrel  5781  coeq1  5842  coeq2  5843  cnveq  5858  dmeq  5888  relssres  6014  xp11  6169  ssrnres  6172  ordtri4  6394  oneqmini  6410  fnres  6670  eqfnfv3  7028  fneqeql2  7042  dff3  7095  fconst4  7211  f1imaeq  7263  eqoprab2bw  7482  eqoprab2b  7483  iunpw  7770  orduniorsuc  7829  tfi  7853  fo1stres  8019  fo2ndres  8020  wfrlem8OLD  8335  tz7.49  8464  oawordeulem  8571  nnacan  8645  nnmcan  8651  ixpeq2  8930  sbthlem3  9104  isinf  9273  isinfOLD  9274  ordunifi  9303  inficl  9442  rankr1c  9840  rankc1  9889  iscard  9994  iscard2  9995  carden2  10006  aleph11  10103  cardaleph  10108  alephinit  10114  dfac12a  10168  cflm  10269  cfslb2n  10287  dfacfin7  10418  wrdeq  14559  isumltss  15869  rpnnen2lem12  16248  isprm2  16706  mrcidb2  17635  smndex2dnrinv  18898  iscyggen2  19867  iscyg3  19872  lssle0  20912  islpir2  21296  iscss2  21651  ishil2  21684  bastop1  22936  epttop  22952  iscld4  23008  0ntr  23014  opnneiid  23069  isperf2  23095  cnntr  23218  ist1-3  23292  perfcls  23308  cmpfi  23351  isconn2  23357  dfconn2  23362  snfil  23807  filconn  23826  ufileu  23862  alexsubALTlem4  23993  metequiv  24453  eqscut2  27775  nbuhgr2vtx1edgblem  29335  iscplgr  29399  shlesb1i  31372  shle0  31428  orthin  31432  chcon2i  31450  chcon3i  31452  chlejb1i  31462  chabs2  31503  h1datomi  31567  cmbr4i  31587  osumcor2i  31630  pjjsi  31686  pjin2i  32179  stcltr2i  32261  mdbr2  32282  dmdbr2  32289  mdsl2i  32308  mdsl2bi  32309  mdslmd3i  32318  chrelat4i  32359  sumdmdlem2  32405  dmdbr5ati  32408  eqdif  32505  eqrelrd2  32601  rspsnasso  33408  dfon2lem9  35814  idsset  35913  fneval  36375  topdifinfeq  37373  equivtotbnd  37807  heiborlem10  37849  eqrel2  38322  relcnveq3  38344  relcnveq2  38346  cossssid  38490  elrelscnveq3  38514  elrelscnveq2  38516  pmap11  39786  dia11N  41072  dia2dimlem5  41092  dib11N  41184  dih11  41289  dihglblem6  41364  doch11  41397  mapd11  41663  mapdcnv11N  41683  sticksstones11  42174  isnacs2  42704  mrefg3  42706  onsupneqmaxlim0  43223  onsupnmax  43227  ontric3g  43521  rababg  43573  relnonrel  43586  uneqsn  44024  ntrk1k3eqk13  44049  ntrneineine1lem  44083  ntrneicls00  44088  ntrneixb  44094  ntrneik13  44097  ntrneix13  44098  joindm2  48922  meetdm2  48924