Theorem eqss 3950

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 1890	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2724	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		df-ss 3919	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3919	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 628	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 303	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541   ∈ wcel 2111   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919

This theorem is referenced by:  eqssi  3951  eqssd  3952  sssseq  3953  sseq1  3960  sseq2  3961  ssrabeq  4034  dfpss3  4039  compleq  4102  uneqin  4239  rcompleq  4255  pssdifn0  4318  ss0b  4351  vss  4396  pwpw0  4765  sssn  4778  ssunsn  4780  unidif  4893  ssunieq  4894  uniintsn  4935  iuneq1  4958  iuneq2  4961  iunxdif2  5002  ssext  5395  pweqb  5397  eqopab2bw  5488  eqopab2b  5492  pwun  5509  soeq2  5546  eqrel  5724  eqrelrel  5737  coeq1  5797  coeq2  5798  cnveq  5813  dmeq  5843  relssres  5971  xp11  6122  ssrnres  6125  ordtri4  6343  oneqmini  6359  fnres  6608  eqfnfv3  6966  fneqeql2  6980  dff3  7033  fconst4  7148  f1imaeq  7199  eqoprab2bw  7416  eqoprab2b  7417  iunpw  7704  orduniorsuc  7760  tfi  7783  fo1stres  7947  fo2ndres  7948  tz7.49  8364  oawordeulem  8469  nnacan  8543  nnmcan  8549  ixpeq2  8835  sbthlem3  9002  isinf  9149  ordunifi  9174  inficl  9309  rankr1c  9714  rankc1  9763  iscard  9868  iscard2  9869  carden2  9880  aleph11  9975  cardaleph  9980  alephinit  9986  dfac12a  10040  cflm  10141  cfslb2n  10159  dfacfin7  10290  wrdeq  14443  isumltss  15755  rpnnen2lem12  16134  isprm2  16593  mrcidb2  17524  smndex2dnrinv  18823  iscyggen2  19794  iscyg3  19799  lssle0  20884  islpir2  21268  iscss2  21624  ishil2  21657  bastop1  22909  epttop  22925  iscld4  22981  0ntr  22987  opnneiid  23042  isperf2  23068  cnntr  23191  ist1-3  23265  perfcls  23281  cmpfi  23324  isconn2  23330  dfconn2  23335  snfil  23780  filconn  23799  ufileu  23835  alexsubALTlem4  23966  metequiv  24425  eqscut2  27748  nbuhgr2vtx1edgblem  29330  iscplgr  29394  shlesb1i  31364  shle0  31420  orthin  31424  chcon2i  31442  chcon3i  31444  chlejb1i  31454  chabs2  31495  h1datomi  31559  cmbr4i  31579  osumcor2i  31622  pjjsi  31678  pjin2i  32171  stcltr2i  32253  mdbr2  32274  dmdbr2  32281  mdsl2i  32300  mdsl2bi  32301  mdslmd3i  32310  chrelat4i  32351  sumdmdlem2  32397  dmdbr5ati  32400  eqdif  32497  eqrelrd2  32597  rspsnasso  33351  dfon2lem9  35831  idsset  35930  fneval  36392  topdifinfeq  37390  equivtotbnd  37824  heiborlem10  37866  eqrel2  38339  relcnveq3  38361  relcnveq2  38363  cossssid  38510  elrelscnveq3  38534  elrelscnveq2  38536  pmap11  39807  dia11N  41093  dia2dimlem5  41113  dib11N  41205  dih11  41310  dihglblem6  41385  doch11  41418  mapd11  41684  mapdcnv11N  41704  sticksstones11  42195  isnacs2  42745  mrefg3  42747  onsupneqmaxlim0  43263  onsupnmax  43267  ontric3g  43561  rababg  43613  relnonrel  43626  uneqsn  44064  ntrk1k3eqk13  44089  ntrneineine1lem  44123  ntrneicls00  44128  ntrneixb  44134  ntrneik13  44137  ntrneix13  44138  joindm2  49005  meetdm2  49007