Theorem eqss 3923

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 1921	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2753	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		df-ss 3896	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3896	. . 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 1567   = wceq 1569   ∈ wcel 2144   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  eqssi  3924  eqssd  3925  sssseq  3926  sseq1  3933  sseq2  3934  ssrabeq  4009  dfpss3  4016  compleq  4088  uneqin  4234  rcompleq  4250  pssdifn0  4315  ss0b  4350  vss  4357  sssn  4781  ssunsn  4783  pwpw0  4830  unidif  4902  ssunieq  4903  uniintsn  4944  iuneq1  4967  iuneq2  4970  iunxdif2  5011  ssext  5421  pweqb  5423  eqopab2bw  5522  eqopab2b  5526  pwun  5543  soeq2  5580  eqrel  5759  eqrelrel  5772  coeq1  5834  coeq2  5835  cnveq  5850  dmeq  5884  relssres  6010  xp11  6166  ssrnres  6169  cnveqb  6189  ordtri4  6400  oneqmini  6416  fnres  6667  eqfnfv3  7032  fneqeql2  7047  dff3  7101  fconst4  7221  f1imaeq  7270  eqoprab2bw  7491  eqoprab2b  7492  iunpw  7786  orduniorsuc  7842  tfi  7865  fo1stres  8028  fo2ndres  8029  tz7.49  8459  oawordeulem  8566  nnacan  8641  nnmcan  8647  ixpeq2  8943  sbthlem3  9112  isinf  9260  ordunifi  9285  inficl  9421  rankr1c  9834  rankc1  9891  iscard  10060  iscard2  10061  carden2  10072  aleph11  10167  cardaleph  10172  alephinit  10178  dfac12a  10231  cflm  10331  cfslb2n  10350  dfacfin7  10481  wrdeq  14685  isumltss  16023  rpnnen2lem12  16399  isprm2  16863  mrcidb2  17798  smndex2dnrinv  19120  iscyggen2  20101  iscyg3  20106  lssle0  21231  islpir2  21660  iscss2  21998  ishil2  22031  bastop1  23317  epttop  23333  iscld4  23389  0ntr  23395  opnneiid  23450  isperf2  23476  cnntr  23599  ist1-3  23673  perfcls  23689  cmpfi  23732  isconn2  23738  dfconn2  23743  snfil  24189  filconn  24208  ufileu  24244  alexsubALTlem4  24375  metequiv  24834  eqcuts2  28178  nbuhgr2vtx1edgblem  29938  iscplgr  30002  shlesb1i  31994  shle0  32050  orthin  32054  chcon2i  32072  chcon3i  32074  chlejb1i  32084  chabs2  32125  h1datomi  32189  cmbr4i  32209  osumcor2i  32252  pjjsi  32308  pjin2i  32801  stcltr2i  32883  mdbr2  32904  dmdbr2  32911  mdsl2i  32930  mdsl2bi  32931  mdslmd3i  32940  chrelat4i  32981  sumdmdlem2  33027  dmdbr5ati  33030  eqdif  33163  eqrelrd2  33258  rspsnasso  33990  fnfvintima  35763  dfon2lem9  36646  idsset  36745  fneval  37233  topdifinfeq  38367  equivtotbnd  38806  heiborlem10  38848  eqrel2  39331  relcnveq3  39353  relcnveq2  39355  cossssid  39583  elrelscnveq3  39653  elrelscnveq2  39655  pmap11  40913  dia11N  42199  dia2dimlem5  42219  dib11N  42311  dih11  42416  dihglblem6  42491  doch11  42524  mapd11  42790  mapdcnv11N  42810  sticksstones11  43300  isnacs2  43811  mrefg3  43813  onsupneqmaxlim0  44320  onsupnmax  44324  ontric3g  44617  rababg  44669  relnonrel  44681  uneqsn  45119  ntrk1k3eqk13  45144  ntrneineine1lem  45178  ntrneicls00  45183  ntrneixb  45189  ntrneik13  45192  ntrneix13  45193  cocan2g  46017  cocan1g  46019  joindm2  50176  meetdm2  50178