Theorem eqssd 3245

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

Syntax hints:   → wi 4   = wceq 1398   ⊆ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  eqrd  3246  eqelssd  3247  unissel  3927  intmin  3953  int0el  3963  pwntru  4295  exmidundif  4302  exmidundifim  4303  dmcosseq  5010  relfld  5272  imadif  5417  imain  5419  fimacnv  5784  fo2ndf  6401  tposeq  6456  tfrlemibfn  6537  tfrlemi14d  6542  tfr1onlembfn  6553  tfri1dALT  6560  tfrcllembfn  6566  dcdifsnid  6715  fisbth  7115  en2eqpr  7142  exmidpw  7143  exmidpweq  7144  undifdcss  7158  nnnninfeq2  7371  en2other2  7450  exmidontriimlem3  7481  pw1m  7485  addnqpr  7824  mulnqpr  7840  distrprg  7851  ltexpri  7876  addcanprg  7879  recexprlemex  7900  aptipr  7904  cauappcvgprlemladd  7921  fzopth  10341  fzosplit  10459  fzouzsplit  10461  zsupssdc  10544  frecuzrdgtcl  10720  frecuzrdgdomlem  10725  ccatrn  11235  phimullem  12860  structcnvcnv  13161  imasaddfnlemg  13460  gsumvallem2  13639  trivsubgd  13850  trivsubgsnd  13851  trivnsgd  13867  kerf1ghm  13924  conjnmz  13929  lspun  14481  lspsn  14495  lspsnneg  14499  lsp0  14502  lsslsp  14508  mulgrhm2  14689  znrrg  14739  eltg4i  14849  unitg  14856  tgtop  14862  tgidm  14868  basgen  14874  2basgeng  14876  epttop  14884  ntrin  14918  isopn3  14919  neiuni  14955  tgrest  14963  resttopon  14965  rest0  14973  txdis  15071  hmeontr  15107  xmettx  15304  findset  16644  pwtrufal  16702  pwf1oexmid  16704