Theorem eqss 3937

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 1896	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2733	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		df-ss 3907	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3907	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 634	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 304	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545   = wceq 1547   ∈ wcel 2119   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  eqssi  3938  eqssd  3939  sssseq  3940  sseq1  3947  sseq2  3948  ssrabeq  4022  dfpss3  4027  compleq  4089  uneqin  4224  rcompleq  4240  pssdifn0  4303  ss0b  4336  vss  4381  pwpw0  4751  sssn  4764  ssunsn  4766  unidif  4880  ssunieq  4881  uniintsn  4922  iuneq1  4945  iuneq2  4948  iunxdif2  4990  ssext  5400  pweqb  5402  eqopab2bw  5497  eqopab2b  5501  pwun  5518  soeq2  5555  eqrel  5734  eqrelrel  5747  coeq1  5806  coeq2  5807  cnveq  5822  dmeq  5852  relssres  5981  xp11  6133  ssrnres  6136  ordtri4  6354  oneqmini  6370  fnres  6619  eqfnfv3  6980  fneqeql2  6995  dff3  7048  fconst4  7165  f1imaeq  7216  eqoprab2bw  7433  eqoprab2b  7434  iunpw  7721  orduniorsuc  7777  tfi  7800  fo1stres  7964  fo2ndres  7965  tz7.49  8381  oawordeulem  8486  nnacan  8561  nnmcan  8567  ixpeq2  8856  sbthlem3  9024  isinf  9172  ordunifi  9197  inficl  9335  rankr1c  9743  rankc1  9792  iscard  9897  iscard2  9898  carden2  9909  aleph11  10004  cardaleph  10009  alephinit  10015  dfac12a  10069  cflm  10170  cfslb2n  10188  dfacfin7  10319  wrdeq  14496  isumltss  15811  rpnnen2lem12  16190  isprm2  16649  mrcidb2  17582  smndex2dnrinv  18884  iscyggen2  19854  iscyg3  19859  lssle0  20947  islpir2  21330  iscss2  21668  ishil2  21701  bastop1  22983  epttop  22999  iscld4  23055  0ntr  23061  opnneiid  23116  isperf2  23142  cnntr  23265  ist1-3  23339  perfcls  23355  cmpfi  23398  isconn2  23404  dfconn2  23409  snfil  23854  filconn  23873  ufileu  23909  alexsubALTlem4  24040  metequiv  24499  eqcuts2  27803  nbuhgr2vtx1edgblem  29445  iscplgr  29509  shlesb1i  31482  shle0  31538  orthin  31542  chcon2i  31560  chcon3i  31562  chlejb1i  31572  chabs2  31613  h1datomi  31677  cmbr4i  31697  osumcor2i  31740  pjjsi  31796  pjin2i  32289  stcltr2i  32371  mdbr2  32392  dmdbr2  32399  mdsl2i  32418  mdsl2bi  32419  mdslmd3i  32428  chrelat4i  32469  sumdmdlem2  32515  dmdbr5ati  32518  eqdif  32614  eqrelrd2  32715  rspsnasso  33478  dfon2lem9  36024  idsset  36123  fneval  36587  topdifinfeq  37719  equivtotbnd  38152  heiborlem10  38194  eqrel2  38679  relcnveq3  38701  relcnveq2  38703  cossssid  38931  elrelscnveq3  39001  elrelscnveq2  39003  pmap11  40261  dia11N  41547  dia2dimlem5  41567  dib11N  41659  dih11  41764  dihglblem6  41839  doch11  41872  mapd11  42138  mapdcnv11N  42158  sticksstones11  42648  isnacs2  43162  mrefg3  43164  onsupneqmaxlim0  43676  onsupnmax  43680  ontric3g  43973  rababg  44025  relnonrel  44038  uneqsn  44476  ntrk1k3eqk13  44501  ntrneineine1lem  44535  ntrneicls00  44540  ntrneixb  44546  ntrneik13  44549  ntrneix13  44550  joindm2  49465  meetdm2  49467