Theorem eqss 3904

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 1871	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2789	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfss2 3877	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3877	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 626	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 304	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1520   = wceq 1522   ∈ wcel 2081   ⊆ wss 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-in 3866  df-ss 3874

This theorem is referenced by:  eqssi  3905  eqssd  3906  sssseq  3907  sseq1  3913  sseq2  3914  eqimss  3944  ssrabeq  3980  dfpss3  3984  compleq  4045  uneqin  4175  pssdifn0  4245  ss0b  4271  vss  4309  pwpw0  4653  sssn  4666  ssunsn  4668  pwsnALT  4738  unidif  4778  ssunieq  4779  uniintsn  4819  iuneq1  4840  iuneq2  4843  iunxdif2  4876  ssext  5239  pweqb  5241  eqopab2b  5327  pwun  5346  soeq2  5383  eqrel  5544  eqrelrel  5556  coeq1  5614  coeq2  5615  cnveq  5630  dmeq  5658  relssres  5774  xp11  5908  ssrnres  5911  ordtri4  6103  oneqmini  6117  fnres  6344  eqfnfv3  6669  fneqeql2  6682  dff3  6729  fconst4  6843  f1imaeq  6888  eqoprab2b  7083  iunpw  7349  orduniorsuc  7401  tfi  7424  fo1stres  7571  fo2ndres  7572  wfrlem8  7814  tz7.49  7932  oawordeulem  8030  nnacan  8104  nnmcan  8110  ixpeq2  8324  sbthlem3  8476  isinf  8577  ordunifi  8614  inficl  8735  rankr1c  9096  rankc1  9145  iscard  9250  iscard2  9251  carden2  9262  aleph11  9356  cardaleph  9361  alephinit  9367  dfac12a  9420  cflm  9518  cfslb2n  9536  dfacfin7  9667  wrdeq  13732  isumltss  15036  rpnnen2lem12  15411  isprm2  15855  mrcidb2  16718  iscyggen2  18723  iscyg3  18728  lssle0  19411  islpir2  19713  iscss2  20512  ishil2  20545  bastop1  21285  epttop  21301  iscld4  21357  0ntr  21363  opnneiid  21418  isperf2  21444  cnntr  21567  ist1-3  21641  perfcls  21657  cmpfi  21700  isconn2  21706  dfconn2  21711  snfil  22156  filconn  22175  ufileu  22211  alexsubALTlem4  22342  metequiv  22802  nbuhgr2vtx1edgblem  26816  iscplgr  26880  shlesb1i  28854  shle0  28910  orthin  28914  chcon2i  28932  chcon3i  28934  chlejb1i  28944  chabs2  28985  h1datomi  29049  cmbr4i  29069  osumcor2i  29112  pjjsi  29168  pjin2i  29661  stcltr2i  29743  mdbr2  29764  dmdbr2  29771  mdsl2i  29790  mdsl2bi  29791  mdslmd3i  29800  chrelat4i  29841  sumdmdlem2  29887  dmdbr5ati  29890  eqdif  29970  eqrelrd2  30057  dfon2lem9  32645  idsset  32961  fneval  33310  topdifinfeq  34181  equivtotbnd  34607  heiborlem10  34649  eqrel2  35108  relcnveq3  35129  relcnveq2  35131  cossssid  35257  elrelscnveq3  35281  elrelscnveq2  35283  pmap11  36448  dia11N  37734  dia2dimlem5  37754  dib11N  37846  dih11  37951  dihglblem6  38026  doch11  38059  mapd11  38325  mapdcnv11N  38345  isnacs2  38807  mrefg3  38809  ontric3g  39392  rababg  39437  relnonrel  39451  rcompleq  39874  uneqsn  39877  ntrk1k3eqk13  39904  ntrneineine1lem  39938  ntrneicls00  39943  ntrneixb  39949  ntrneik13  39952  ntrneix13  39953