Theorem eqss 3938

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542   ∈ wcel 2114   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  eqssi  3939  eqssd  3940  sssseq  3941  sseq1  3948  sseq2  3949  ssrabeq  4025  dfpss3  4030  compleq  4093  uneqin  4230  rcompleq  4246  pssdifn0  4309  ss0b  4342  vss  4387  pwpw0  4757  sssn  4770  ssunsn  4772  unidif  4886  ssunieq  4887  uniintsn  4928  iuneq1  4951  iuneq2  4954  iunxdif2  4997  ssext  5401  pweqb  5403  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  6979  fneqeql2  6993  dff3  7046  fconst4  7162  f1imaeq  7213  eqoprab2bw  7430  eqoprab2b  7431  iunpw  7718  orduniorsuc  7774  tfi  7797  fo1stres  7961  fo2ndres  7962  tz7.49  8377  oawordeulem  8482  nnacan  8557  nnmcan  8563  ixpeq2  8852  sbthlem3  9020  isinf  9168  ordunifi  9193  inficl  9331  rankr1c  9736  rankc1  9785  iscard  9890  iscard2  9891  carden2  9902  aleph11  9997  cardaleph  10002  alephinit  10008  dfac12a  10062  cflm  10163  cfslb2n  10181  dfacfin7  10312  wrdeq  14489  isumltss  15804  rpnnen2lem12  16183  isprm2  16642  mrcidb2  17575  smndex2dnrinv  18877  iscyggen2  19847  iscyg3  19852  lssle0  20936  islpir2  21320  iscss2  21676  ishil2  21709  bastop1  22968  epttop  22984  iscld4  23040  0ntr  23046  opnneiid  23101  isperf2  23127  cnntr  23250  ist1-3  23324  perfcls  23340  cmpfi  23383  isconn2  23389  dfconn2  23394  snfil  23839  filconn  23858  ufileu  23894  alexsubALTlem4  24025  metequiv  24484  eqcuts2  27792  nbuhgr2vtx1edgblem  29434  iscplgr  29498  shlesb1i  31472  shle0  31528  orthin  31532  chcon2i  31550  chcon3i  31552  chlejb1i  31562  chabs2  31603  h1datomi  31667  cmbr4i  31687  osumcor2i  31730  pjjsi  31786  pjin2i  32279  stcltr2i  32361  mdbr2  32382  dmdbr2  32389  mdsl2i  32408  mdsl2bi  32409  mdslmd3i  32418  chrelat4i  32459  sumdmdlem2  32505  dmdbr5ati  32508  eqdif  32604  eqrelrd2  32704  rspsnasso  33463  dfon2lem9  35987  idsset  36086  fneval  36550  topdifinfeq  37680  equivtotbnd  38113  heiborlem10  38155  eqrel2  38640  relcnveq3  38662  relcnveq2  38664  cossssid  38892  elrelscnveq3  38962  elrelscnveq2  38964  pmap11  40222  dia11N  41508  dia2dimlem5  41528  dib11N  41620  dih11  41725  dihglblem6  41800  doch11  41833  mapd11  42099  mapdcnv11N  42119  sticksstones11  42609  isnacs2  43152  mrefg3  43154  onsupneqmaxlim0  43670  onsupnmax  43674  ontric3g  43967  rababg  44019  relnonrel  44032  uneqsn  44470  ntrk1k3eqk13  44495  ntrneineine1lem  44529  ntrneicls00  44534  ntrneixb  44540  ntrneik13  44543  ntrneix13  44544  joindm2  49455  meetdm2  49457