Theorem eqssd 3196

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  eqrd  3197  eqelssd  3198  unissel  3864  intmin  3890  int0el  3900  pwntru  4228  exmidundif  4235  exmidundifim  4236  dmcosseq  4933  relfld  5194  imadif  5334  imain  5336  fimacnv  5687  fo2ndf  6280  tposeq  6300  tfrlemibfn  6381  tfrlemi14d  6386  tfr1onlembfn  6397  tfri1dALT  6404  tfrcllembfn  6410  dcdifsnid  6557  fisbth  6939  en2eqpr  6963  exmidpw  6964  exmidpweq  6965  undifdcss  6979  nnnninfeq2  7188  en2other2  7256  exmidontriimlem3  7283  addnqpr  7621  mulnqpr  7637  distrprg  7648  ltexpri  7673  addcanprg  7676  recexprlemex  7697  aptipr  7701  cauappcvgprlemladd  7718  fzopth  10127  fzosplit  10244  fzouzsplit  10246  frecuzrdgtcl  10483  frecuzrdgdomlem  10488  zsupssdc  12091  phimullem  12363  structcnvcnv  12634  imasaddfnlemg  12897  gsumvallem2  13065  trivsubgd  13270  trivsubgsnd  13271  trivnsgd  13287  kerf1ghm  13344  conjnmz  13349  lspun  13898  lspsn  13912  lspsnneg  13916  lsp0  13919  lsslsp  13925  mulgrhm2  14098  znrrg  14148  eltg4i  14223  unitg  14230  tgtop  14236  tgidm  14242  basgen  14248  2basgeng  14250  epttop  14258  ntrin  14292  isopn3  14293  neiuni  14329  tgrest  14337  resttopon  14339  rest0  14347  txdis  14445  hmeontr  14481  xmettx  14678  findset  15437  pwtrufal  15488  pwf1oexmid  15490