Theorem eqssi 3619

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	|- A C_ B
eqssi.2	|- B C_ A

Assertion

Ref	Expression
eqssi	|- A = B

Proof of Theorem eqssi

Step	Hyp	Ref	Expression
1		eqssi.1	. 2 |- A C_ B
2		eqssi.2	. 2 |- B C_ A
3		eqss 3618	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
4	1, 2, 3	mpbir2an 955	1 |- A = B

Syntax hints:   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  inv1  3970  unv  3971  intab  4507  intabs  4825  intid  4926  dmv  5341  0ima  5482  fresaunres2  6076  find  7091  dftpos4  7371  wfrlem16  7430  dfom3  8544  tc2  8618  tcidm  8622  tc0  8623  rankuni  8726  rankval4  8730  ackbij1  9060  cfom  9086  fin23lem16  9157  itunitc  9243  inaprc  9658  nqerf  9752  dmrecnq  9790  dmaddsr  9906  dmmulsr  9907  axaddf  9966  axmulf  9967  dfnn2  11033  dfuzi  11468  unirnioo  12273  uzrdgfni  12757  0bits  15161  4sqlem19  15667  ledm  17224  lern  17225  efgsfo  18152  0frgp  18192  indiscld  20895  leordtval2  21016  lecldbas  21023  llyidm  21291  nllyidm  21292  toplly  21293  lly1stc  21299  txuni2  21368  txindis  21437  ust0  22023  qdensere  22573  xrtgioo  22609  zdis  22619  xrhmeo  22745  bndth  22757  ismbf3d  23421  dvef  23743  reeff1o  24201  efifo  24293  dvloglem  24394  logf1o2  24396  choc1  28186  shsidmi  28243  shsval2i  28246  omlsii  28262  chdmm1i  28336  chj1i  28348  chm0i  28349  shjshsi  28351  span0  28401  spanuni  28403  sshhococi  28405  spansni  28416  pjoml4i  28446  pjrni  28561  shatomistici  29220  sumdmdlem2  29278  rinvf1o  29432  sigapildsys  30225  sxbrsigalem0  30333  dya2iocucvr  30346  sxbrsigalem4  30349  sxbrsiga  30352  ballotth  30599  kur14lem6  31193  mrsubrn  31410  msubrn  31426  filnetlem3  32375  filnetlem4  32376  onint1  32448  oninhaus  32449  bj-rabtr  32926  bj-rabtrALTALT  32928  bj-rabtrAUTO  32929  bj-disj2r  33013  bj-nuliotaALT  33020  icoreunrn  33207  idinxpres  34088  comptiunov2i  37998  compneOLD  38644  unisnALT  39162  fsumiunss  39807  fourierdlem62  40385  fouriersw  40448  salexct  40552  salgencntex  40561