Theorem eqssd 3201

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

Syntax hints:   → wi 4   = wceq 1364   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  eqrd  3202  eqelssd  3203  unissel  3869  intmin  3895  int0el  3905  pwntru  4233  exmidundif  4240  exmidundifim  4241  dmcosseq  4938  relfld  5199  imadif  5339  imain  5341  fimacnv  5694  fo2ndf  6294  tposeq  6314  tfrlemibfn  6395  tfrlemi14d  6400  tfr1onlembfn  6411  tfri1dALT  6418  tfrcllembfn  6424  dcdifsnid  6571  fisbth  6953  en2eqpr  6977  exmidpw  6978  exmidpweq  6979  undifdcss  6993  nnnninfeq2  7204  en2other2  7277  exmidontriimlem3  7308  addnqpr  7647  mulnqpr  7663  distrprg  7674  ltexpri  7699  addcanprg  7702  recexprlemex  7723  aptipr  7727  cauappcvgprlemladd  7744  fzopth  10155  fzosplit  10272  fzouzsplit  10274  zsupssdc  10347  frecuzrdgtcl  10523  frecuzrdgdomlem  10528  phimullem  12420  structcnvcnv  12721  imasaddfnlemg  13018  gsumvallem2  13197  trivsubgd  13408  trivsubgsnd  13409  trivnsgd  13425  kerf1ghm  13482  conjnmz  13487  lspun  14036  lspsn  14050  lspsnneg  14054  lsp0  14057  lsslsp  14063  mulgrhm2  14244  znrrg  14294  eltg4i  14399  unitg  14406  tgtop  14412  tgidm  14418  basgen  14424  2basgeng  14426  epttop  14434  ntrin  14468  isopn3  14469  neiuni  14505  tgrest  14513  resttopon  14515  rest0  14523  txdis  14621  hmeontr  14657  xmettx  14854  findset  15699  pwtrufal  15752  pwf1oexmid  15754