Theorem eqss 3946

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 1922	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2754	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		df-ss 3916	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3916	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 640	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 306	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570   ∈ wcel 2145   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  eqssi  3947  eqssd  3948  sssseq  3949  sseq1  3956  sseq2  3957  ssrabeq  4032  dfpss3  4037  compleq  4099  uneqin  4235  rcompleq  4251  pssdifn0  4316  ss0b  4351  vss  4358  pwpw0  4774  sssn  4787  ssunsn  4789  unidif  4903  ssunieq  4904  uniintsn  4945  iuneq1  4968  iuneq2  4971  iunxdif2  5012  ssext  5422  pweqb  5424  eqopab2bw  5523  eqopab2b  5527  pwun  5544  soeq2  5581  eqrel  5760  eqrelrel  5773  coeq1  5835  coeq2  5836  cnveq  5851  dmeq  5885  relssres  6013  xp11  6166  ssrnres  6169  ordtri4  6393  oneqmini  6409  fnres  6658  eqfnfv3  7023  fneqeql2  7038  dff3  7092  fconst4  7212  f1imaeq  7261  eqoprab2bw  7482  eqoprab2b  7483  iunpw  7774  orduniorsuc  7830  tfi  7853  fo1stres  8016  fo2ndres  8017  tz7.49  8439  oawordeulem  8546  nnacan  8621  nnmcan  8627  ixpeq2  8923  sbthlem3  9092  isinf  9240  ordunifi  9265  inficl  9401  rankr1c  9811  rankc1  9868  iscard  10037  iscard2  10038  carden2  10049  aleph11  10144  cardaleph  10149  alephinit  10155  dfac12a  10208  cflm  10308  cfslb2n  10327  dfacfin7  10458  wrdeq  14661  isumltss  15997  rpnnen2lem12  16373  isprm2  16837  mrcidb2  17772  smndex2dnrinv  19094  iscyggen2  20075  iscyg3  20080  lssle0  21205  islpir2  21634  iscss2  21972  ishil2  22005  bastop1  23291  epttop  23307  iscld4  23363  0ntr  23369  opnneiid  23424  isperf2  23450  cnntr  23573  ist1-3  23647  perfcls  23663  cmpfi  23706  isconn2  23712  dfconn2  23717  snfil  24163  filconn  24182  ufileu  24218  alexsubALTlem4  24349  metequiv  24808  eqcuts2  28154  nbuhgr2vtx1edgblem  29914  iscplgr  29978  shlesb1i  31970  shle0  32026  orthin  32030  chcon2i  32048  chcon3i  32050  chlejb1i  32060  chabs2  32101  h1datomi  32165  cmbr4i  32185  osumcor2i  32228  pjjsi  32284  pjin2i  32777  stcltr2i  32859  mdbr2  32880  dmdbr2  32887  mdsl2i  32906  mdsl2bi  32907  mdslmd3i  32916  chrelat4i  32957  sumdmdlem2  33003  dmdbr5ati  33006  eqdif  33097  eqrelrd2  33192  rspsnasso  33925  fnfvintima  35695  dfon2lem9  36523  idsset  36622  fneval  37110  topdifinfeq  38241  equivtotbnd  38680  heiborlem10  38722  eqrel2  39205  relcnveq3  39227  relcnveq2  39229  cossssid  39457  elrelscnveq3  39527  elrelscnveq2  39529  pmap11  40787  dia11N  42073  dia2dimlem5  42093  dib11N  42185  dih11  42290  dihglblem6  42365  doch11  42398  mapd11  42664  mapdcnv11N  42684  sticksstones11  43174  isnacs2  43670  mrefg3  43672  onsupneqmaxlim0  44184  onsupnmax  44188  ontric3g  44481  rababg  44533  relnonrel  44546  uneqsn  44984  ntrk1k3eqk13  45009  ntrneineine1lem  45043  ntrneicls00  45048  ntrneixb  45054  ntrneik13  45057  ntrneix13  45058  joindm2  50020  meetdm2  50022