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  7275  exmidontriimlem3  7306  addnqpr  7645  mulnqpr  7661  distrprg  7672  ltexpri  7697  addcanprg  7700  recexprlemex  7721  aptipr  7725  cauappcvgprlemladd  7742  fzopth  10153  fzosplit  10270  fzouzsplit  10272  zsupssdc  10345  frecuzrdgtcl  10521  frecuzrdgdomlem  10526  phimullem  12418  structcnvcnv  12719  imasaddfnlemg  13016  gsumvallem2  13195  trivsubgd  13406  trivsubgsnd  13407  trivnsgd  13423  kerf1ghm  13480  conjnmz  13485  lspun  14034  lspsn  14048  lspsnneg  14052  lsp0  14055  lsslsp  14061  mulgrhm2  14242  znrrg  14292  eltg4i  14375  unitg  14382  tgtop  14388  tgidm  14394  basgen  14400  2basgeng  14402  epttop  14410  ntrin  14444  isopn3  14445  neiuni  14481  tgrest  14489  resttopon  14491  rest0  14499  txdis  14597  hmeontr  14633  xmettx  14830  findset  15675  pwtrufal  15728  pwf1oexmid  15730