Theorem eqss 3955

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 2759	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		df-ss 3925	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3925	. . 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 2146   ⊆ wss 3908

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 2156  ax-ext 2738

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

This theorem is used by:  eqssi  3956  eqssd  3957  sssseq  3958  sseq1  3965  sseq2  3966  ssrabeq  4041  dfpss3  4046  compleq  4109  uneqin  4245  rcompleq  4261  pssdifn0  4326  ss0b  4361  vss  4368  pwpw0  4784  sssn  4797  ssunsn  4799  unidif  4913  ssunieq  4914  uniintsn  4955  iuneq1  4978  iuneq2  4981  iunxdif2  5023  ssext  5440  pweqb  5442  eqopab2bw  5538  eqopab2b  5542  pwun  5559  soeq2  5596  eqrel  5775  eqrelrel  5788  coeq1  5848  coeq2  5849  cnveq  5864  dmeq  5898  relssres  6026  xp11  6178  ssrnres  6181  ordtri4  6405  oneqmini  6421  fnres  6669  eqfnfv3  7034  fneqeql2  7049  dff3  7102  fconst4  7219  f1imaeq  7270  eqoprab2bw  7493  eqoprab2b  7494  iunpw  7779  orduniorsuc  7835  tfi  7858  fo1stres  8021  fo2ndres  8022  tz7.49  8441  oawordeulem  8548  nnacan  8623  nnmcan  8629  ixpeq2  8918  sbthlem3  9087  isinf  9235  ordunifi  9260  inficl  9395  rankr1c  9803  rankc1  9852  iscard  9980  iscard2  9981  carden2  9992  aleph11  10087  cardaleph  10092  alephinit  10098  dfac12a  10151  cflm  10251  cfslb2n  10270  dfacfin7  10401  wrdeq  14593  isumltss  15928  rpnnen2lem12  16306  isprm2  16765  mrcidb2  17699  smndex2dnrinv  19008  iscyggen2  19982  iscyg3  19987  lssle0  21108  islpir2  21535  iscss2  21873  ishil2  21906  bastop1  23187  epttop  23203  iscld4  23259  0ntr  23265  opnneiid  23320  isperf2  23346  cnntr  23469  ist1-3  23543  perfcls  23559  cmpfi  23602  isconn2  23608  dfconn2  23613  snfil  24058  filconn  24077  ufileu  24113  alexsubALTlem4  24244  metequiv  24703  eqcuts2  28016  nbuhgr2vtx1edgblem  29738  iscplgr  29802  shlesb1i  31775  shle0  31831  orthin  31835  chcon2i  31853  chcon3i  31855  chlejb1i  31865  chabs2  31906  h1datomi  31970  cmbr4i  31990  osumcor2i  32033  pjjsi  32089  pjin2i  32582  stcltr2i  32664  mdbr2  32685  dmdbr2  32692  mdsl2i  32711  mdsl2bi  32712  mdslmd3i  32721  chrelat4i  32762  sumdmdlem2  32808  dmdbr5ati  32811  eqdif  32902  eqrelrd2  32998  rspsnasso  33732  fnfvintima  35502  dfon2lem9  36302  idsset  36401  fneval  36904  topdifinfeq  38037  equivtotbnd  38470  heiborlem10  38512  eqrel2  38995  relcnveq3  39017  relcnveq2  39019  cossssid  39247  elrelscnveq3  39317  elrelscnveq2  39319  pmap11  40577  dia11N  41863  dia2dimlem5  41883  dib11N  41975  dih11  42080  dihglblem6  42155  doch11  42188  mapd11  42454  mapdcnv11N  42474  sticksstones11  42964  isnacs2  43478  mrefg3  43480  onsupneqmaxlim0  43992  onsupnmax  43996  ontric3g  44289  rababg  44341  relnonrel  44354  uneqsn  44792  ntrk1k3eqk13  44817  ntrneineine1lem  44851  ntrneicls00  44856  ntrneixb  44862  ntrneik13  44865  ntrneix13  44866  joindm2  49787  meetdm2  49789