Theorem eqssd 3200

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 3198	. 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  3201  eqelssd  3202  unissel  3868  intmin  3894  int0el  3904  pwntru  4232  exmidundif  4239  exmidundifim  4240  dmcosseq  4937  relfld  5198  imadif  5338  imain  5340  fimacnv  5691  fo2ndf  6285  tposeq  6305  tfrlemibfn  6386  tfrlemi14d  6391  tfr1onlembfn  6402  tfri1dALT  6409  tfrcllembfn  6415  dcdifsnid  6562  fisbth  6944  en2eqpr  6968  exmidpw  6969  exmidpweq  6970  undifdcss  6984  nnnninfeq2  7195  en2other2  7263  exmidontriimlem3  7290  addnqpr  7628  mulnqpr  7644  distrprg  7655  ltexpri  7680  addcanprg  7683  recexprlemex  7704  aptipr  7708  cauappcvgprlemladd  7725  fzopth  10136  fzosplit  10253  fzouzsplit  10255  zsupssdc  10328  frecuzrdgtcl  10504  frecuzrdgdomlem  10509  phimullem  12393  structcnvcnv  12694  imasaddfnlemg  12957  gsumvallem2  13125  trivsubgd  13330  trivsubgsnd  13331  trivnsgd  13347  kerf1ghm  13404  conjnmz  13409  lspun  13958  lspsn  13972  lspsnneg  13976  lsp0  13979  lsslsp  13985  mulgrhm2  14166  znrrg  14216  eltg4i  14291  unitg  14298  tgtop  14304  tgidm  14310  basgen  14316  2basgeng  14318  epttop  14326  ntrin  14360  isopn3  14361  neiuni  14397  tgrest  14405  resttopon  14407  rest0  14415  txdis  14513  hmeontr  14549  xmettx  14746  findset  15591  pwtrufal  15642  pwf1oexmid  15644