Theorem eqssd 3241

Description: Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.)

Hypotheses

Ref	Expression
eqssd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
eqssd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐴)

Assertion

Ref	Expression
eqssd	⊢ (𝜑 → 𝐴 = 𝐵)

Proof of Theorem eqssd

Step	Hyp	Ref	Expression
1		eqssd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		eqssd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
3		eqss 3239	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
4	1, 2, 3	sylanbrc 417	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1395   ⊆ wss 3197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  eqrd  3242  eqelssd  3243  unissel  3916  intmin  3942  int0el  3952  pwntru  4282  exmidundif  4289  exmidundifim  4290  dmcosseq  4995  relfld  5256  imadif  5400  imain  5402  fimacnv  5763  fo2ndf  6371  tposeq  6391  tfrlemibfn  6472  tfrlemi14d  6477  tfr1onlembfn  6488  tfri1dALT  6495  tfrcllembfn  6501  dcdifsnid  6648  fisbth  7041  en2eqpr  7065  exmidpw  7066  exmidpweq  7067  undifdcss  7081  nnnninfeq2  7292  en2other2  7370  exmidontriimlem3  7401  pw1m  7405  addnqpr  7744  mulnqpr  7760  distrprg  7771  ltexpri  7796  addcanprg  7799  recexprlemex  7820  aptipr  7824  cauappcvgprlemladd  7841  fzopth  10253  fzosplit  10371  fzouzsplit  10373  zsupssdc  10453  frecuzrdgtcl  10629  frecuzrdgdomlem  10634  ccatrn  11139  phimullem  12742  structcnvcnv  13043  imasaddfnlemg  13342  gsumvallem2  13521  trivsubgd  13732  trivsubgsnd  13733  trivnsgd  13749  kerf1ghm  13806  conjnmz  13811  lspun  14360  lspsn  14374  lspsnneg  14378  lsp0  14381  lsslsp  14387  mulgrhm2  14568  znrrg  14618  eltg4i  14723  unitg  14730  tgtop  14736  tgidm  14742  basgen  14748  2basgeng  14750  epttop  14758  ntrin  14792  isopn3  14793  neiuni  14829  tgrest  14837  resttopon  14839  rest0  14847  txdis  14945  hmeontr  14981  xmettx  15178  findset  16266  pwtrufal  16322  pwf1oexmid  16324