Theorem eqss 3985

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 2818	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfss2 3958	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3958	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 628	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 305	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1534   = wceq 1536   ∈ wcel 2113   ⊆ wss 3939

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-in 3946  df-ss 3955

This theorem is referenced by:  eqssi  3986  eqssd  3987  sssseq  3988  sseq1  3995  sseq2  3996  eqimss  4026  ssrabeq  4062  dfpss3  4066  compleq  4127  uneqin  4258  pssdifn0  4328  ss0b  4354  vss  4398  pwpw0  4749  sssn  4762  ssunsn  4764  pwsnOLD  4834  unidif  4875  ssunieq  4876  uniintsn  4916  iuneq1  4938  iuneq2  4941  iunxdif2  4980  ssext  5350  pweqb  5352  eqopab2bw  5438  eqopab2b  5442  pwun  5461  soeq2  5498  eqrel  5661  eqrelrel  5673  coeq1  5731  coeq2  5732  cnveq  5747  dmeq  5775  relssres  5896  xp11  6035  ssrnres  6038  ordtri4  6231  oneqmini  6245  fnres  6477  eqfnfv3  6807  fneqeql2  6820  dff3  6869  fconst4  6980  f1imaeq  7026  eqoprab2bw  7227  eqoprab2b  7228  iunpw  7496  orduniorsuc  7548  tfi  7571  fo1stres  7718  fo2ndres  7719  wfrlem8  7965  tz7.49  8084  oawordeulem  8183  nnacan  8257  nnmcan  8263  ixpeq2  8478  sbthlem3  8632  isinf  8734  ordunifi  8771  inficl  8892  rankr1c  9253  rankc1  9302  iscard  9407  iscard2  9408  carden2  9419  aleph11  9513  cardaleph  9518  alephinit  9524  dfac12a  9577  cflm  9675  cfslb2n  9693  dfacfin7  9824  wrdeq  13889  isumltss  15206  rpnnen2lem12  15581  isprm2  16029  mrcidb2  16892  smndex2dnrinv  18083  iscyggen2  19003  iscyg3  19008  lssle0  19724  islpir2  20027  iscss2  20833  ishil2  20866  bastop1  21604  epttop  21620  iscld4  21676  0ntr  21682  opnneiid  21737  isperf2  21763  cnntr  21886  ist1-3  21960  perfcls  21976  cmpfi  22019  isconn2  22025  dfconn2  22030  snfil  22475  filconn  22494  ufileu  22530  alexsubALTlem4  22661  metequiv  23122  nbuhgr2vtx1edgblem  27136  iscplgr  27200  shlesb1i  29166  shle0  29222  orthin  29226  chcon2i  29244  chcon3i  29246  chlejb1i  29256  chabs2  29297  h1datomi  29361  cmbr4i  29381  osumcor2i  29424  pjjsi  29480  pjin2i  29973  stcltr2i  30055  mdbr2  30076  dmdbr2  30083  mdsl2i  30102  mdsl2bi  30103  mdslmd3i  30112  chrelat4i  30153  sumdmdlem2  30199  dmdbr5ati  30202  eqdif  30284  eqrelrd2  30370  dfon2lem9  33040  idsset  33355  fneval  33704  topdifinfeq  34635  equivtotbnd  35060  heiborlem10  35102  eqrel2  35561  relcnveq3  35582  relcnveq2  35584  cossssid  35711  elrelscnveq3  35735  elrelscnveq2  35737  pmap11  36902  dia11N  38188  dia2dimlem5  38208  dib11N  38300  dih11  38405  dihglblem6  38480  doch11  38513  mapd11  38779  mapdcnv11N  38799  isnacs2  39309  mrefg3  39311  ontric3g  39894  rababg  39939  relnonrel  39953  rcompleq  40376  uneqsn  40379  ntrk1k3eqk13  40406  ntrneineine1lem  40440  ntrneicls00  40445  ntrneixb  40451  ntrneik13  40454  ntrneix13  40455