Theorem eqssd 3218

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

Syntax hints:   → wi 4   = wceq 1373   ⊆ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  eqrd  3219  eqelssd  3220  unissel  3893  intmin  3919  int0el  3929  pwntru  4259  exmidundif  4266  exmidundifim  4267  dmcosseq  4969  relfld  5230  imadif  5373  imain  5375  fimacnv  5732  fo2ndf  6336  tposeq  6356  tfrlemibfn  6437  tfrlemi14d  6442  tfr1onlembfn  6453  tfri1dALT  6460  tfrcllembfn  6466  dcdifsnid  6613  fisbth  7006  en2eqpr  7030  exmidpw  7031  exmidpweq  7032  undifdcss  7046  nnnninfeq2  7257  en2other2  7335  exmidontriimlem3  7366  pw1m  7370  addnqpr  7709  mulnqpr  7725  distrprg  7736  ltexpri  7761  addcanprg  7764  recexprlemex  7785  aptipr  7789  cauappcvgprlemladd  7806  fzopth  10218  fzosplit  10336  fzouzsplit  10338  zsupssdc  10418  frecuzrdgtcl  10594  frecuzrdgdomlem  10599  ccatrn  11103  phimullem  12662  structcnvcnv  12963  imasaddfnlemg  13261  gsumvallem2  13440  trivsubgd  13651  trivsubgsnd  13652  trivnsgd  13668  kerf1ghm  13725  conjnmz  13730  lspun  14279  lspsn  14293  lspsnneg  14297  lsp0  14300  lsslsp  14306  mulgrhm2  14487  znrrg  14537  eltg4i  14642  unitg  14649  tgtop  14655  tgidm  14661  basgen  14667  2basgeng  14669  epttop  14677  ntrin  14711  isopn3  14712  neiuni  14748  tgrest  14756  resttopon  14758  rest0  14766  txdis  14864  hmeontr  14900  xmettx  15097  findset  16080  pwtrufal  16136  pwf1oexmid  16138