Theorem eqssd 3209

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

Syntax hints:   → wi 4   = wceq 1372   ⊆ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  eqrd  3210  eqelssd  3211  unissel  3878  intmin  3904  int0el  3914  pwntru  4242  exmidundif  4249  exmidundifim  4250  dmcosseq  4949  relfld  5210  imadif  5353  imain  5355  fimacnv  5708  fo2ndf  6312  tposeq  6332  tfrlemibfn  6413  tfrlemi14d  6418  tfr1onlembfn  6429  tfri1dALT  6436  tfrcllembfn  6442  dcdifsnid  6589  fisbth  6979  en2eqpr  7003  exmidpw  7004  exmidpweq  7005  undifdcss  7019  nnnninfeq2  7230  en2other2  7303  exmidontriimlem3  7334  addnqpr  7673  mulnqpr  7689  distrprg  7700  ltexpri  7725  addcanprg  7728  recexprlemex  7749  aptipr  7753  cauappcvgprlemladd  7770  fzopth  10182  fzosplit  10299  fzouzsplit  10301  zsupssdc  10379  frecuzrdgtcl  10555  frecuzrdgdomlem  10560  ccatrn  11063  phimullem  12518  structcnvcnv  12819  imasaddfnlemg  13117  gsumvallem2  13296  trivsubgd  13507  trivsubgsnd  13508  trivnsgd  13524  kerf1ghm  13581  conjnmz  13586  lspun  14135  lspsn  14149  lspsnneg  14153  lsp0  14156  lsslsp  14162  mulgrhm2  14343  znrrg  14393  eltg4i  14498  unitg  14505  tgtop  14511  tgidm  14517  basgen  14523  2basgeng  14525  epttop  14533  ntrin  14567  isopn3  14568  neiuni  14604  tgrest  14612  resttopon  14614  rest0  14622  txdis  14720  hmeontr  14756  xmettx  14953  findset  15843  pwtrufal  15896  pwf1oexmid  15898