Theorem eqssd 3265

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 3263	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
4	1, 2, 3	sylanbrc 421	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1402   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  eqrd  3266  eqelssd  3267  unissel  3959  intmin  3985  int0el  3995  pwntru  4331  exmidundif  4338  exmidundifim  4339  dmcosseq  5049  relfld  5311  imadif  5456  imain  5458  fimacnv  5828  fo2ndf  6453  tposeq  6508  tfrlemibfn  6589  tfrlemi14d  6594  tfr1onlembfn  6605  tfri1dALT  6612  tfrcllembfn  6618  dcdifsnid  6767  fisbth  7177  en2eqpr  7204  exmidpw  7205  exmidpweq  7206  undifdcss  7220  nnnninfeq2  7459  en2other2  7538  exmidontriimlem3  7569  pw1m  7573  addnqpr  7918  mulnqpr  7934  distrprg  7945  ltexpri  7970  addcanprg  7973  recexprlemex  7994  aptipr  7998  cauappcvgprlemladd  8015  fzopth  10445  fzosplit  10564  fzouzsplit  10566  zsupssdc  10651  frecuzrdgtcl  10827  frecuzrdgdomlem  10832  ccatrn  11355  phimullem  12981  structcnvcnv  13346  imasaddfnlemg  13612  gsumvallem2  13777  trivsubgd  13980  trivsubgsnd  13981  trivnsgd  13997  kerf1ghm  14054  conjnmz  14059  lspun  14711  lspsn  14725  lspsnneg  14729  lsp0  14732  lsslsp  14738  mulgrhm2  14917  znrrg  14967  eltg4i  15079  unitg  15086  tgtop  15092  tgidm  15098  basgen  15104  2basgeng  15106  epttop  15114  ntrin  15148  isopn3  15149  neiuni  15185  tgrest  15193  resttopon  15195  rest0  15203  txdis  15301  hmeontr  15337  xmettx  15534  findset  16885  pwtrufal  16941  pwf1oexmid  16943