Theorem eqssd 3244

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

Syntax hints:   → wi 4   = wceq 1397   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  eqrd  3245  eqelssd  3246  unissel  3922  intmin  3948  int0el  3958  pwntru  4289  exmidundif  4296  exmidundifim  4297  dmcosseq  5004  relfld  5265  imadif  5410  imain  5412  fimacnv  5776  fo2ndf  6391  tposeq  6412  tfrlemibfn  6493  tfrlemi14d  6498  tfr1onlembfn  6509  tfri1dALT  6516  tfrcllembfn  6522  dcdifsnid  6671  fisbth  7071  en2eqpr  7098  exmidpw  7099  exmidpweq  7100  undifdcss  7114  nnnninfeq2  7327  en2other2  7406  exmidontriimlem3  7437  pw1m  7441  addnqpr  7780  mulnqpr  7796  distrprg  7807  ltexpri  7832  addcanprg  7835  recexprlemex  7856  aptipr  7860  cauappcvgprlemladd  7877  fzopth  10295  fzosplit  10413  fzouzsplit  10415  zsupssdc  10497  frecuzrdgtcl  10673  frecuzrdgdomlem  10678  ccatrn  11185  phimullem  12796  structcnvcnv  13097  imasaddfnlemg  13396  gsumvallem2  13575  trivsubgd  13786  trivsubgsnd  13787  trivnsgd  13803  kerf1ghm  13860  conjnmz  13865  lspun  14415  lspsn  14429  lspsnneg  14433  lsp0  14436  lsslsp  14442  mulgrhm2  14623  znrrg  14673  eltg4i  14778  unitg  14785  tgtop  14791  tgidm  14797  basgen  14803  2basgeng  14805  epttop  14813  ntrin  14847  isopn3  14848  neiuni  14884  tgrest  14892  resttopon  14894  rest0  14902  txdis  15000  hmeontr  15036  xmettx  15233  findset  16540  pwtrufal  16598  pwf1oexmid  16600