Theorem eqssi 3939

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 3938	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
4	1, 2, 3	mpbir2an 712	1 ⊢ 𝐴 = 𝐵

Syntax hints:   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  inv1  4339  unv  4340  intab  4921  intabs  5287  dmv  5872  0ima  6038  cnvrescnv  6154  find  7840  dftpos4  8189  dfom3  9562  dmttrcl  9636  rnttrcl  9637  tc2  9655  tcidm  9659  tc0  9660  rankuni  9781  rankval4  9785  djuunxp  9839  djuun  9844  ackbij1  10153  cfom  10180  fin23lem16  10251  itunitc  10337  inaprc  10753  nqerf  10847  dmrecnq  10885  dmaddsr  11002  dmmulsr  11003  axaddf  11062  axmulf  11063  dfnn2  12181  dfuzi  12614  unirnioo  13396  uzrdgfni  13914  0bits  16402  4sqlem19  16928  ledm  18550  lern  18551  efgsfo  19708  0frgp  19748  indiscld  23069  leordtval2  23190  lecldbas  23197  llyidm  23466  nllyidm  23467  toplly  23468  lly1stc  23474  txuni2  23543  txindis  23612  ust0  24198  qdensere  24747  xrtgioo  24785  zdis  24795  xrhmeo  24926  bndth  24938  ismbf3d  25634  dvef  25960  reeff1o  26428  efifo  26527  dvloglem  26628  logf1o2  26630  bday1  27823  oniso  28280  dfn0s2  28341  bdayn0sf1o  28379  dfnns2  28381  choc1  31416  shsidmi  31473  shsval2i  31476  omlsii  31492  chdmm1i  31566  chj1i  31578  chm0i  31579  shjshsi  31581  span0  31631  spanuni  31633  sshhococi  31635  spansni  31646  pjoml4i  31676  pjrni  31791  shatomistici  32450  sumdmdlem2  32508  rinvf1o  32721  sigapildsys  34325  sxbrsigalem0  34434  dya2iocucvr  34447  sxbrsigalem4  34450  sxbrsiga  34453  ballotth  34701  kur14lem6  35412  mrsubrn  35714  msubrn  35730  filnetlem3  36581  filnetlem4  36582  onint1  36650  oninhaus  36651  ttcuniun  36711  ttciunun  36712  ttcuni  36714  dfttc4  36731  bj-rabtr  37256  bj-rabtrAUTO  37258  bj-disj2r  37354  bj-nuliotaALT  37384  bj-idres  37493  icoreunrn  37692  dmsucmap  38806  comptiunov2i  44154  unisnALT  45373  fsumiunss  46026  fourierdlem62  46617  fouriersw  46680  salexct  46783  salgencntex  46792