Theorem eqss 3651

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 1856	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2645	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfss2 3624	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3624	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 733	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 292	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1521   = wceq 1523   ∈ wcel 2030   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621

This theorem is referenced by:  eqssi  3652  eqssd  3653  sssseq  3654  sseq1  3659  sseq2  3660  eqimss  3690  ssrabeq  3722  dfpss3  3726  compleq  3785  uneqin  3911  pssdifn0  3977  ss0b  4006  vss  4045  pwpw0  4376  sssn  4390  ssunsn  4392  pwsnALT  4461  unidif  4503  ssunieq  4504  uniintsn  4546  iuneq1  4566  iuneq2  4569  iunxdif2  4600  ssext  4953  pweqb  4955  eqopab2b  5034  pwun  5051  soeq2  5084  eqrel  5243  eqrelrel  5255  coeq1  5312  coeq2  5313  cnveq  5328  dmeq  5356  relssres  5472  xp11  5604  ssrnres  5607  ordtri4  5799  oneqmini  5814  fnres  6045  eqfnfv3  6353  fneqeql2  6366  dff3  6412  fconst4  6519  f1imaeq  6562  eqoprab2b  6755  iunpw  7020  orduniorsuc  7072  tfi  7095  fo1stres  7236  fo2ndres  7237  wfrlem8  7467  tz7.49  7585  oawordeulem  7679  nnacan  7753  nnmcan  7759  ixpeq2  7964  sbthlem3  8113  isinf  8214  ordunifi  8251  inficl  8372  rankr1c  8722  rankc1  8771  iscard  8839  iscard2  8840  carden2  8851  aleph11  8945  cardaleph  8950  alephinit  8956  dfac12a  9008  cflm  9110  cfslb2n  9128  dfacfin7  9259  wrdeq  13359  isumltss  14624  rpnnen2lem12  14998  isprm2  15442  mrcidb2  16325  iscyggen2  18329  iscyg3  18334  lssle0  18998  islpir2  19299  iscss2  20078  ishil2  20111  bastop1  20845  epttop  20861  iscld4  20917  0ntr  20923  opnneiid  20978  isperf2  21004  cnntr  21127  ist1-3  21201  perfcls  21217  cmpfi  21259  isconn2  21265  dfconn2  21270  snfil  21715  filconn  21734  ufileu  21770  alexsubALTlem4  21901  metequiv  22361  nbuhgr2vtx1edgblem  26292  iscplgr  26366  shlesb1i  28373  shle0  28429  orthin  28433  chcon2i  28451  chcon3i  28453  chlejb1i  28463  chabs2  28504  h1datomi  28568  cmbr4i  28588  osumcor2i  28631  pjjsi  28687  pjin2i  29180  stcltr2i  29262  mdbr2  29283  dmdbr2  29290  mdsl2i  29309  mdsl2bi  29310  mdslmd3i  29319  chrelat4i  29360  sumdmdlem2  29406  dmdbr5ati  29409  eqrelrd2  29554  dfon2lem9  31820  idsset  32122  fneval  32472  topdifinfeq  33328  equivtotbnd  33707  heiborlem10  33749  eqrel2  34209  relcnveq3  34233  relcnveq2  34235  cossssid  34357  elrelscnveq3  34381  elrelscnveq2  34383  pmap11  35366  dia11N  36654  dia2dimlem5  36674  dib11N  36766  dih11  36871  dihglblem6  36946  doch11  36979  mapd11  37245  mapdcnv11N  37265  isnacs2  37586  mrefg3  37588  rababg  38196  relnonrel  38210  rcompleq  38635  uneqsn  38638  ntrk1k3eqk13  38665  ntrneineine1lem  38699  ntrneicls00  38704  ntrneixb  38710  ntrneik13  38713  ntrneix13  38714  prsal  40856