Theorem eqss 3949

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 1908	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
2		dfcleq 2754	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		df-ss 3919	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3919	. . 3 ⊢ (𝐵 ⊆ 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴))
5	3, 4	anbi12i 637	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	1, 2, 5	3bitr4i 305	1 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1557   = wceq 1559   ∈ wcel 2141   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919

This theorem is referenced by:  eqssi  3950  eqssd  3951  sssseq  3952  sseq1  3959  sseq2  3960  ssrabeq  4035  dfpss3  4040  compleq  4103  uneqin  4239  rcompleq  4255  pssdifn0  4318  ss0b  4352  vss  4397  pwpw0  4768  sssn  4781  ssunsn  4783  unidif  4898  ssunieq  4899  uniintsn  4940  iuneq1  4963  iuneq2  4966  iunxdif2  5008  ssext  5418  pweqb  5420  eqopab2bw  5515  eqopab2b  5519  pwun  5536  soeq2  5573  eqrel  5752  eqrelrel  5765  coeq1  5825  coeq2  5826  cnveq  5841  dmeq  5875  relssres  6004  xp11  6155  ssrnres  6158  ordtri4  6377  oneqmini  6393  fnres  6642  eqfnfv3  7007  fneqeql2  7022  dff3  7075  fconst4  7192  f1imaeq  7243  eqoprab2bw  7460  eqoprab2b  7461  iunpw  7748  orduniorsuc  7804  tfi  7827  fo1stres  7990  fo2ndres  7991  tz7.49  8409  oawordeulem  8516  nnacan  8591  nnmcan  8597  ixpeq2  8886  sbthlem3  9054  isinf  9202  ordunifi  9227  inficl  9364  rankr1c  9772  rankc1  9821  iscard  9926  iscard2  9927  carden2  9938  aleph11  10033  cardaleph  10038  alephinit  10044  dfac12a  10098  cflm  10199  cfslb2n  10218  dfacfin7  10349  wrdeq  14542  isumltss  15868  rpnnen2lem12  16247  isprm2  16706  mrcidb2  17640  smndex2dnrinv  18942  iscyggen2  19911  iscyg3  19916  lssle0  21004  islpir2  21387  iscss2  21725  ishil2  21758  bastop1  23040  epttop  23056  iscld4  23112  0ntr  23118  opnneiid  23173  isperf2  23199  cnntr  23322  ist1-3  23396  perfcls  23412  cmpfi  23455  isconn2  23461  dfconn2  23466  snfil  23911  filconn  23930  ufileu  23966  alexsubALTlem4  24097  metequiv  24556  eqcuts2  27866  nbuhgr2vtx1edgblem  29508  iscplgr  29572  shlesb1i  31545  shle0  31601  orthin  31605  chcon2i  31623  chcon3i  31625  chlejb1i  31635  chabs2  31676  h1datomi  31740  cmbr4i  31760  osumcor2i  31803  pjjsi  31859  pjin2i  32352  stcltr2i  32434  mdbr2  32455  dmdbr2  32462  mdsl2i  32481  mdsl2bi  32482  mdslmd3i  32491  chrelat4i  32532  sumdmdlem2  32578  dmdbr5ati  32581  eqdif  32677  eqrelrd2  32778  rspsnasso  33534  dfon2lem9  36099  idsset  36198  fneval  36672  topdifinfeq  37804  equivtotbnd  38237  heiborlem10  38279  eqrel2  38764  relcnveq3  38786  relcnveq2  38788  cossssid  39016  elrelscnveq3  39086  elrelscnveq2  39088  pmap11  40346  dia11N  41632  dia2dimlem5  41652  dib11N  41744  dih11  41849  dihglblem6  41924  doch11  41957  mapd11  42223  mapdcnv11N  42243  sticksstones11  42733  isnacs2  43247  mrefg3  43249  onsupneqmaxlim0  43761  onsupnmax  43765  ontric3g  44058  rababg  44110  relnonrel  44123  uneqsn  44561  ntrk1k3eqk13  44586  ntrneineine1lem  44620  ntrneicls00  44625  ntrneixb  44631  ntrneik13  44634  ntrneix13  44635  joindm2  49549  meetdm2  49551