Theorem eqssd 3241

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

Syntax hints:   → wi 4   = wceq 1395   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  eqrd  3242  eqelssd  3243  unissel  3917  intmin  3943  int0el  3953  pwntru  4283  exmidundif  4290  exmidundifim  4291  dmcosseq  4996  relfld  5257  imadif  5401  imain  5403  fimacnv  5766  fo2ndf  6379  tposeq  6399  tfrlemibfn  6480  tfrlemi14d  6485  tfr1onlembfn  6496  tfri1dALT  6503  tfrcllembfn  6509  dcdifsnid  6658  fisbth  7053  en2eqpr  7080  exmidpw  7081  exmidpweq  7082  undifdcss  7096  nnnninfeq2  7307  en2other2  7385  exmidontriimlem3  7416  pw1m  7420  addnqpr  7759  mulnqpr  7775  distrprg  7786  ltexpri  7811  addcanprg  7814  recexprlemex  7835  aptipr  7839  cauappcvgprlemladd  7856  fzopth  10269  fzosplit  10387  fzouzsplit  10389  zsupssdc  10470  frecuzrdgtcl  10646  frecuzrdgdomlem  10651  ccatrn  11157  phimullem  12762  structcnvcnv  13063  imasaddfnlemg  13362  gsumvallem2  13541  trivsubgd  13752  trivsubgsnd  13753  trivnsgd  13769  kerf1ghm  13826  conjnmz  13831  lspun  14381  lspsn  14395  lspsnneg  14399  lsp0  14402  lsslsp  14408  mulgrhm2  14589  znrrg  14639  eltg4i  14744  unitg  14751  tgtop  14757  tgidm  14763  basgen  14769  2basgeng  14771  epttop  14779  ntrin  14813  isopn3  14814  neiuni  14850  tgrest  14858  resttopon  14860  rest0  14868  txdis  14966  hmeontr  15002  xmettx  15199  findset  16363  pwtrufal  16422  pwf1oexmid  16424