Theorem eqssd 3159

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

Syntax hints:   → wi 4   = wceq 1343   ⊆ wss 3116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3122  df-ss 3129

This theorem is referenced by:  eqrd  3160  eqelssd  3161  unissel  3818  intmin  3844  int0el  3854  pwntru  4178  exmidundif  4185  exmidundifim  4186  dmcosseq  4875  relfld  5132  imadif  5268  imain  5270  fimacnv  5614  fo2ndf  6195  tposeq  6215  tfrlemibfn  6296  tfrlemi14d  6301  tfr1onlembfn  6312  tfri1dALT  6319  tfrcllembfn  6325  dcdifsnid  6472  fisbth  6849  en2eqpr  6873  exmidpw  6874  exmidpweq  6875  undifdcss  6888  nnnninfeq2  7093  en2other2  7152  exmidontriimlem3  7179  addnqpr  7502  mulnqpr  7518  distrprg  7529  ltexpri  7554  addcanprg  7557  recexprlemex  7578  aptipr  7582  cauappcvgprlemladd  7599  fzopth  9996  fzosplit  10112  fzouzsplit  10114  frecuzrdgtcl  10347  frecuzrdgdomlem  10352  zsupssdc  11887  phimullem  12157  structcnvcnv  12410  eltg4i  12695  unitg  12702  tgtop  12708  tgidm  12714  basgen  12720  2basgeng  12722  epttop  12730  ntrin  12764  isopn3  12765  neiuni  12801  tgrest  12809  resttopon  12811  rest0  12819  txdis  12917  hmeontr  12953  xmettx  13150  findset  13827  pwtrufal  13877  pwf1oexmid  13879