Theorem eqssd 3259

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  eqrd  3260  eqelssd  3261  unissel  3948  intmin  3974  int0el  3984  pwntru  4317  exmidundif  4324  exmidundifim  4325  dmcosseq  5034  relfld  5296  imadif  5441  imain  5443  fimacnv  5811  fo2ndf  6436  tposeq  6491  tfrlemibfn  6572  tfrlemi14d  6577  tfr1onlembfn  6588  tfri1dALT  6595  tfrcllembfn  6601  dcdifsnid  6750  fisbth  7153  en2eqpr  7180  exmidpw  7181  exmidpweq  7182  undifdcss  7196  nnnninfeq2  7433  en2other2  7512  exmidontriimlem3  7543  pw1m  7547  addnqpr  7892  mulnqpr  7908  distrprg  7919  ltexpri  7944  addcanprg  7947  recexprlemex  7968  aptipr  7972  cauappcvgprlemladd  7989  fzopth  10416  fzosplit  10535  fzouzsplit  10537  zsupssdc  10622  frecuzrdgtcl  10798  frecuzrdgdomlem  10803  ccatrn  11322  phimullem  12947  structcnvcnv  13312  imasaddfnlemg  13578  gsumvallem2  13748  trivsubgd  13953  trivsubgsnd  13954  trivnsgd  13970  kerf1ghm  14027  conjnmz  14032  lspun  14676  lspsn  14690  lspsnneg  14694  lsp0  14697  lsslsp  14703  mulgrhm2  14884  znrrg  14934  eltg4i  15046  unitg  15053  tgtop  15059  tgidm  15065  basgen  15071  2basgeng  15073  epttop  15081  ntrin  15115  isopn3  15116  neiuni  15152  tgrest  15160  resttopon  15162  rest0  15170  txdis  15268  hmeontr  15304  xmettx  15501  findset  16841  pwtrufal  16897  pwf1oexmid  16899