Theorem eqss 3962

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  eqssi  3963  eqssd  3964  sssseq  3965  sseq1  3972  sseq2  3973  ssrabeq  4047  dfpss3  4052  compleq  4115  uneqin  4252  rcompleq  4268  pssdifn0  4331  ss0b  4364  vss  4409  pwpw0  4777  sssn  4790  ssunsn  4792  unidif  4906  ssunieq  4907  uniintsn  4949  iuneq1  4972  iuneq2  4975  iunxdif2  5017  ssext  5414  pweqb  5416  eqopab2bw  5508  eqopab2b  5512  pwun  5531  soeq2  5568  eqrel  5747  eqrelrel  5760  coeq1  5821  coeq2  5822  cnveq  5837  dmeq  5867  relssres  5993  xp11  6148  ssrnres  6151  ordtri4  6369  oneqmini  6385  fnres  6645  eqfnfv3  7005  fneqeql2  7019  dff3  7072  fconst4  7188  f1imaeq  7240  eqoprab2bw  7459  eqoprab2b  7460  iunpw  7747  orduniorsuc  7805  tfi  7829  fo1stres  7994  fo2ndres  7995  tz7.49  8413  oawordeulem  8518  nnacan  8592  nnmcan  8598  ixpeq2  8884  sbthlem3  9053  isinf  9207  isinfOLD  9208  ordunifi  9237  inficl  9376  rankr1c  9774  rankc1  9823  iscard  9928  iscard2  9929  carden2  9940  aleph11  10037  cardaleph  10042  alephinit  10048  dfac12a  10102  cflm  10203  cfslb2n  10221  dfacfin7  10352  wrdeq  14501  isumltss  15814  rpnnen2lem12  16193  isprm2  16652  mrcidb2  17579  smndex2dnrinv  18842  iscyggen2  19811  iscyg3  19816  lssle0  20856  islpir2  21240  iscss2  21595  ishil2  21628  bastop1  22880  epttop  22896  iscld4  22952  0ntr  22958  opnneiid  23013  isperf2  23039  cnntr  23162  ist1-3  23236  perfcls  23252  cmpfi  23295  isconn2  23301  dfconn2  23306  snfil  23751  filconn  23770  ufileu  23806  alexsubALTlem4  23937  metequiv  24397  eqscut2  27718  nbuhgr2vtx1edgblem  29278  iscplgr  29342  shlesb1i  31315  shle0  31371  orthin  31375  chcon2i  31393  chcon3i  31395  chlejb1i  31405  chabs2  31446  h1datomi  31510  cmbr4i  31530  osumcor2i  31573  pjjsi  31629  pjin2i  32122  stcltr2i  32204  mdbr2  32225  dmdbr2  32232  mdsl2i  32251  mdsl2bi  32252  mdslmd3i  32261  chrelat4i  32302  sumdmdlem2  32348  dmdbr5ati  32351  eqdif  32448  eqrelrd2  32544  rspsnasso  33359  dfon2lem9  35779  idsset  35878  fneval  36340  topdifinfeq  37338  equivtotbnd  37772  heiborlem10  37814  eqrel2  38287  relcnveq3  38309  relcnveq2  38311  cossssid  38458  elrelscnveq3  38482  elrelscnveq2  38484  pmap11  39756  dia11N  41042  dia2dimlem5  41062  dib11N  41154  dih11  41259  dihglblem6  41334  doch11  41367  mapd11  41633  mapdcnv11N  41653  sticksstones11  42144  isnacs2  42694  mrefg3  42696  onsupneqmaxlim0  43213  onsupnmax  43217  ontric3g  43511  rababg  43563  relnonrel  43576  uneqsn  44014  ntrk1k3eqk13  44039  ntrneineine1lem  44073  ntrneicls00  44078  ntrneixb  44084  ntrneik13  44087  ntrneix13  44088  joindm2  48956  meetdm2  48958