Theorem eqss 3953

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

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 2701

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

This theorem is referenced by:  eqssi  3954  eqssd  3955  sssseq  3956  sseq1  3963  sseq2  3964  ssrabeq  4037  dfpss3  4042  compleq  4105  uneqin  4242  rcompleq  4258  pssdifn0  4321  ss0b  4354  vss  4399  pwpw0  4767  sssn  4780  ssunsn  4782  unidif  4895  ssunieq  4896  uniintsn  4938  iuneq1  4961  iuneq2  4964  iunxdif2  5005  ssext  5401  pweqb  5403  eqopab2bw  5495  eqopab2b  5499  pwun  5516  soeq2  5553  eqrel  5731  eqrelrel  5744  coeq1  5804  coeq2  5805  cnveq  5820  dmeq  5850  relssres  5977  xp11  6128  ssrnres  6131  ordtri4  6348  oneqmini  6364  fnres  6613  eqfnfv3  6971  fneqeql2  6985  dff3  7038  fconst4  7154  f1imaeq  7206  eqoprab2bw  7423  eqoprab2b  7424  iunpw  7711  orduniorsuc  7769  tfi  7793  fo1stres  7957  fo2ndres  7958  tz7.49  8374  oawordeulem  8479  nnacan  8553  nnmcan  8559  ixpeq2  8845  sbthlem3  9013  isinf  9165  isinfOLD  9166  ordunifi  9195  inficl  9334  rankr1c  9736  rankc1  9785  iscard  9890  iscard2  9891  carden2  9902  aleph11  9997  cardaleph  10002  alephinit  10008  dfac12a  10062  cflm  10163  cfslb2n  10181  dfacfin7  10312  wrdeq  14461  isumltss  15773  rpnnen2lem12  16152  isprm2  16611  mrcidb2  17542  smndex2dnrinv  18807  iscyggen2  19778  iscyg3  19783  lssle0  20871  islpir2  21255  iscss2  21611  ishil2  21644  bastop1  22896  epttop  22912  iscld4  22968  0ntr  22974  opnneiid  23029  isperf2  23055  cnntr  23178  ist1-3  23252  perfcls  23268  cmpfi  23311  isconn2  23317  dfconn2  23322  snfil  23767  filconn  23786  ufileu  23822  alexsubALTlem4  23953  metequiv  24413  eqscut2  27735  nbuhgr2vtx1edgblem  29314  iscplgr  29378  shlesb1i  31348  shle0  31404  orthin  31408  chcon2i  31426  chcon3i  31428  chlejb1i  31438  chabs2  31479  h1datomi  31543  cmbr4i  31563  osumcor2i  31606  pjjsi  31662  pjin2i  32155  stcltr2i  32237  mdbr2  32258  dmdbr2  32265  mdsl2i  32284  mdsl2bi  32285  mdslmd3i  32294  chrelat4i  32335  sumdmdlem2  32381  dmdbr5ati  32384  eqdif  32481  eqrelrd2  32577  rspsnasso  33338  dfon2lem9  35767  idsset  35866  fneval  36328  topdifinfeq  37326  equivtotbnd  37760  heiborlem10  37802  eqrel2  38275  relcnveq3  38297  relcnveq2  38299  cossssid  38446  elrelscnveq3  38470  elrelscnveq2  38472  pmap11  39744  dia11N  41030  dia2dimlem5  41050  dib11N  41142  dih11  41247  dihglblem6  41322  doch11  41355  mapd11  41621  mapdcnv11N  41641  sticksstones11  42132  isnacs2  42682  mrefg3  42684  onsupneqmaxlim0  43200  onsupnmax  43204  ontric3g  43498  rababg  43550  relnonrel  43563  uneqsn  44001  ntrk1k3eqk13  44026  ntrneineine1lem  44060  ntrneicls00  44065  ntrneixb  44071  ntrneik13  44074  ntrneix13  44075  joindm2  48956  meetdm2  48958