Theorem eqss 3949

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 2729	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		df-ss 3918	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3918	. . 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 2113   ⊆ wss 3901

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 2123  ax-ext 2708

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

This theorem is referenced by:  eqssi  3950  eqssd  3951  sssseq  3952  sseq1  3959  sseq2  3960  ssrabeq  4036  dfpss3  4041  compleq  4104  uneqin  4241  rcompleq  4257  pssdifn0  4320  ss0b  4353  vss  4398  pwpw0  4769  sssn  4782  ssunsn  4784  unidif  4898  ssunieq  4899  uniintsn  4940  iuneq1  4963  iuneq2  4966  iunxdif2  5009  ssext  5402  pweqb  5404  eqopab2bw  5496  eqopab2b  5500  pwun  5517  soeq2  5554  eqrel  5733  eqrelrel  5746  coeq1  5806  coeq2  5807  cnveq  5822  dmeq  5852  relssres  5981  xp11  6133  ssrnres  6136  ordtri4  6354  oneqmini  6370  fnres  6619  eqfnfv3  6978  fneqeql2  6992  dff3  7045  fconst4  7160  f1imaeq  7211  eqoprab2bw  7428  eqoprab2b  7429  iunpw  7716  orduniorsuc  7772  tfi  7795  fo1stres  7959  fo2ndres  7960  tz7.49  8376  oawordeulem  8481  nnacan  8556  nnmcan  8562  ixpeq2  8849  sbthlem3  9017  isinf  9165  ordunifi  9190  inficl  9328  rankr1c  9733  rankc1  9782  iscard  9887  iscard2  9888  carden2  9899  aleph11  9994  cardaleph  9999  alephinit  10005  dfac12a  10059  cflm  10160  cfslb2n  10178  dfacfin7  10309  wrdeq  14459  isumltss  15771  rpnnen2lem12  16150  isprm2  16609  mrcidb2  17541  smndex2dnrinv  18840  iscyggen2  19810  iscyg3  19815  lssle0  20901  islpir2  21285  iscss2  21641  ishil2  21674  bastop1  22937  epttop  22953  iscld4  23009  0ntr  23015  opnneiid  23070  isperf2  23096  cnntr  23219  ist1-3  23293  perfcls  23309  cmpfi  23352  isconn2  23358  dfconn2  23363  snfil  23808  filconn  23827  ufileu  23863  alexsubALTlem4  23994  metequiv  24453  eqcuts2  27782  nbuhgr2vtx1edgblem  29424  iscplgr  29488  shlesb1i  31461  shle0  31517  orthin  31521  chcon2i  31539  chcon3i  31541  chlejb1i  31551  chabs2  31592  h1datomi  31656  cmbr4i  31676  osumcor2i  31719  pjjsi  31775  pjin2i  32268  stcltr2i  32350  mdbr2  32371  dmdbr2  32378  mdsl2i  32397  mdsl2bi  32398  mdslmd3i  32407  chrelat4i  32448  sumdmdlem2  32494  dmdbr5ati  32497  eqdif  32594  eqrelrd2  32694  rspsnasso  33469  dfon2lem9  35983  idsset  36082  fneval  36546  topdifinfeq  37555  equivtotbnd  37979  heiborlem10  38021  eqrel2  38498  relcnveq3  38520  relcnveq2  38522  cossssid  38730  elrelscnveq3  38800  elrelscnveq2  38802  pmap11  40022  dia11N  41308  dia2dimlem5  41328  dib11N  41420  dih11  41525  dihglblem6  41600  doch11  41633  mapd11  41899  mapdcnv11N  41919  sticksstones11  42410  isnacs2  42948  mrefg3  42950  onsupneqmaxlim0  43466  onsupnmax  43470  ontric3g  43763  rababg  43815  relnonrel  43828  uneqsn  44266  ntrk1k3eqk13  44291  ntrneineine1lem  44325  ntrneicls00  44330  ntrneixb  44336  ntrneik13  44339  ntrneix13  44340  joindm2  49213  meetdm2  49215