Theorem eqss 3937

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

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 2708

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

This theorem is referenced by:  eqssi  3938  eqssd  3939  sssseq  3940  sseq1  3947  sseq2  3948  ssrabeq  4024  dfpss3  4029  compleq  4092  uneqin  4229  rcompleq  4245  pssdifn0  4308  ss0b  4341  vss  4386  pwpw0  4756  sssn  4769  ssunsn  4771  unidif  4885  ssunieq  4886  uniintsn  4927  iuneq1  4950  iuneq2  4953  iunxdif2  4996  ssext  5406  pweqb  5408  eqopab2bw  5503  eqopab2b  5507  pwun  5524  soeq2  5561  eqrel  5740  eqrelrel  5753  coeq1  5812  coeq2  5813  cnveq  5828  dmeq  5858  relssres  5987  xp11  6139  ssrnres  6142  ordtri4  6360  oneqmini  6376  fnres  6625  eqfnfv3  6985  fneqeql2  6999  dff3  7052  fconst4  7169  f1imaeq  7220  eqoprab2bw  7437  eqoprab2b  7438  iunpw  7725  orduniorsuc  7781  tfi  7804  fo1stres  7968  fo2ndres  7969  tz7.49  8384  oawordeulem  8489  nnacan  8564  nnmcan  8570  ixpeq2  8859  sbthlem3  9027  isinf  9175  ordunifi  9200  inficl  9338  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  14498  isumltss  15813  rpnnen2lem12  16192  isprm2  16651  mrcidb2  17584  smndex2dnrinv  18886  iscyggen2  19856  iscyg3  19861  lssle0  20945  islpir2  21328  iscss2  21666  ishil2  21699  bastop1  22958  epttop  22974  iscld4  23030  0ntr  23036  opnneiid  23091  isperf2  23117  cnntr  23240  ist1-3  23314  perfcls  23330  cmpfi  23373  isconn2  23379  dfconn2  23384  snfil  23829  filconn  23848  ufileu  23884  alexsubALTlem4  24015  metequiv  24474  eqcuts2  27778  nbuhgr2vtx1edgblem  29420  iscplgr  29484  shlesb1i  31457  shle0  31513  orthin  31517  chcon2i  31535  chcon3i  31537  chlejb1i  31547  chabs2  31588  h1datomi  31652  cmbr4i  31672  osumcor2i  31715  pjjsi  31771  pjin2i  32264  stcltr2i  32346  mdbr2  32367  dmdbr2  32374  mdsl2i  32393  mdsl2bi  32394  mdslmd3i  32403  chrelat4i  32444  sumdmdlem2  32490  dmdbr5ati  32493  eqdif  32589  eqrelrd2  32689  rspsnasso  33448  dfon2lem9  35971  idsset  36070  fneval  36534  topdifinfeq  37666  equivtotbnd  38099  heiborlem10  38141  eqrel2  38626  relcnveq3  38648  relcnveq2  38650  cossssid  38878  elrelscnveq3  38948  elrelscnveq2  38950  pmap11  40208  dia11N  41494  dia2dimlem5  41514  dib11N  41606  dih11  41711  dihglblem6  41786  doch11  41819  mapd11  42085  mapdcnv11N  42105  sticksstones11  42595  isnacs2  43138  mrefg3  43140  onsupneqmaxlim0  43652  onsupnmax  43656  ontric3g  43949  rababg  44001  relnonrel  44014  uneqsn  44452  ntrk1k3eqk13  44477  ntrneineine1lem  44511  ntrneicls00  44516  ntrneixb  44522  ntrneik13  44525  ntrneix13  44526  joindm2  49443  meetdm2  49445