Theorem eqssi 3584

Description: Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.)

Hypotheses

Ref	Expression
eqssi.1	⊢ 𝐴 ⊆ 𝐵
eqssi.2	⊢ 𝐵 ⊆ 𝐴

Assertion

Ref	Expression
eqssi	⊢ 𝐴 = 𝐵

Proof of Theorem eqssi

Step	Hyp	Ref	Expression
1		eqssi.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		eqssi.2	. 2 ⊢ 𝐵 ⊆ 𝐴
3		eqss 3583	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
4	1, 2, 3	mpbir2an 957	1 ⊢ 𝐴 = 𝐵

Syntax hints:   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  inv1  3922  unv  3923  intab  4442  intabs  4752  intid  4853  dmv  5262  0ima  5401  fresaunres2  5989  find  6983  dftpos4  7258  wfrlem16  7317  dfom3  8427  tc2  8501  tcidm  8505  tc0  8506  rankuni  8609  rankval4  8613  ackbij1  8943  cfom  8969  fin23lem16  9040  itunitc  9126  inaprc  9537  nqerf  9631  dmrecnq  9669  dmaddsr  9785  dmmulsr  9786  axaddf  9845  axmulf  9846  dfnn2  10910  dfuzi  11344  unirnioo  12144  uzrdgfni  12619  0bits  14999  4sqlem19  15505  ledm  17047  lern  17048  efgsfo  17975  0frgp  18015  indiscld  20705  leordtval2  20826  lecldbas  20833  llyidm  21101  nllyidm  21102  toplly  21103  lly1stc  21109  txuni2  21178  txindis  21247  ust0  21833  qdensere  22383  xrtgioo  22417  zdis  22427  xrhmeo  22553  bndth  22565  ismbf3d  23227  dvef  23547  reeff1o  24005  efifo  24097  dvloglem  24194  logf1o2  24196  choc1  27570  shsidmi  27627  shsval2i  27630  omlsii  27646  chdmm1i  27720  chj1i  27732  chm0i  27733  shjshsi  27735  span0  27785  spanuni  27787  sshhococi  27789  spansni  27800  pjoml4i  27830  pjrni  27945  shatomistici  28604  sumdmdlem2  28662  rinvf1o  28814  sigapildsys  29552  sxbrsigalem0  29660  dya2iocucvr  29673  sxbrsigalem4  29676  sxbrsiga  29679  ballotth  29926  kur14lem6  30447  mrsubrn  30664  msubrn  30680  filnetlem3  31545  filnetlem4  31546  onint1  31618  oninhaus  31619  bj-rabtr  32118  bj-rabtrALTALT  32120  bj-rabtrAUTO  32121  bj-nuliotaALT  32211  icoreunrn  32383  comptiunov2i  37017  compne  37665  unisnALT  38184  fsumiunss  38642  fourierdlem62  39061  fouriersw  39124  salexct  39228  salgencntex  39237