Theorem eqss 4010

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1534   = wceq 1536   ∈ wcel 2105   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  eqssi  4011  eqssd  4012  sssseq  4013  sseq1  4020  sseq2  4021  ssrabeq  4093  dfpss3  4098  compleq  4161  uneqin  4294  rcompleq  4310  pssdifn0  4373  ss0b  4406  vss  4451  pwpw0  4817  sssn  4830  ssunsn  4832  unidif  4946  ssunieq  4947  uniintsn  4989  iuneq1  5012  iuneq2  5015  iunxdif2  5057  ssext  5464  pweqb  5466  eqopab2bw  5557  eqopab2b  5561  pwun  5580  soeq2  5618  eqrel  5796  eqrelrel  5809  coeq1  5870  coeq2  5871  cnveq  5886  dmeq  5916  relssres  6041  xp11  6196  ssrnres  6199  ordtri4  6422  oneqmini  6437  fnres  6695  eqfnfv3  7052  fneqeql2  7066  dff3  7119  fconst4  7233  f1imaeq  7284  eqoprab2bw  7502  eqoprab2b  7503  iunpw  7789  orduniorsuc  7849  tfi  7873  fo1stres  8038  fo2ndres  8039  wfrlem8OLD  8354  tz7.49  8483  oawordeulem  8590  nnacan  8664  nnmcan  8670  ixpeq2  8949  sbthlem3  9123  isinf  9293  isinfOLD  9294  ordunifi  9323  inficl  9462  rankr1c  9858  rankc1  9907  iscard  10012  iscard2  10013  carden2  10024  aleph11  10121  cardaleph  10126  alephinit  10132  dfac12a  10186  cflm  10287  cfslb2n  10305  dfacfin7  10436  wrdeq  14570  isumltss  15880  rpnnen2lem12  16257  isprm2  16715  mrcidb2  17662  smndex2dnrinv  18940  iscyggen2  19913  iscyg3  19918  lssle0  20965  islpir2  21357  iscss2  21721  ishil2  21756  bastop1  23015  epttop  23031  iscld4  23088  0ntr  23094  opnneiid  23149  isperf2  23175  cnntr  23298  ist1-3  23372  perfcls  23388  cmpfi  23431  isconn2  23437  dfconn2  23442  snfil  23887  filconn  23906  ufileu  23942  alexsubALTlem4  24073  metequiv  24537  eqscut2  27865  nbuhgr2vtx1edgblem  29382  iscplgr  29446  shlesb1i  31414  shle0  31470  orthin  31474  chcon2i  31492  chcon3i  31494  chlejb1i  31504  chabs2  31545  h1datomi  31609  cmbr4i  31629  osumcor2i  31672  pjjsi  31728  pjin2i  32221  stcltr2i  32303  mdbr2  32324  dmdbr2  32331  mdsl2i  32350  mdsl2bi  32351  mdslmd3i  32360  chrelat4i  32401  sumdmdlem2  32447  dmdbr5ati  32450  eqdif  32546  eqrelrd2  32635  rspsnasso  33395  dfon2lem9  35772  idsset  35871  fneval  36334  topdifinfeq  37332  equivtotbnd  37764  heiborlem10  37806  eqrel2  38280  relcnveq3  38302  relcnveq2  38304  cossssid  38448  elrelscnveq3  38472  elrelscnveq2  38474  pmap11  39744  dia11N  41030  dia2dimlem5  41050  dib11N  41142  dih11  41247  dihglblem6  41322  doch11  41355  mapd11  41621  mapdcnv11N  41641  sticksstones11  42137  isnacs2  42693  mrefg3  42695  onsupneqmaxlim0  43212  onsupnmax  43216  ontric3g  43511  rababg  43563  relnonrel  43576  uneqsn  44014  ntrk1k3eqk13  44039  ntrneineine1lem  44073  ntrneicls00  44078  ntrneixb  44084  ntrneik13  44087  ntrneix13  44088  joindm2  48764  meetdm2  48766