Theorem eqssd 3173

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

Syntax hints:   → wi 4   = wceq 1353   ⊆ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  eqrd  3174  eqelssd  3175  unissel  3839  intmin  3865  int0el  3875  pwntru  4200  exmidundif  4207  exmidundifim  4208  dmcosseq  4899  relfld  5158  imadif  5297  imain  5299  fimacnv  5646  fo2ndf  6228  tposeq  6248  tfrlemibfn  6329  tfrlemi14d  6334  tfr1onlembfn  6345  tfri1dALT  6352  tfrcllembfn  6358  dcdifsnid  6505  fisbth  6883  en2eqpr  6907  exmidpw  6908  exmidpweq  6909  undifdcss  6922  nnnninfeq2  7127  en2other2  7195  exmidontriimlem3  7222  addnqpr  7560  mulnqpr  7576  distrprg  7587  ltexpri  7612  addcanprg  7615  recexprlemex  7636  aptipr  7640  cauappcvgprlemladd  7657  fzopth  10061  fzosplit  10177  fzouzsplit  10179  frecuzrdgtcl  10412  frecuzrdgdomlem  10417  zsupssdc  11955  phimullem  12225  structcnvcnv  12478  imasaddfnlemg  12735  trivsubgd  13060  trivsubgsnd  13061  trivnsgd  13077  eltg4i  13558  unitg  13565  tgtop  13571  tgidm  13577  basgen  13583  2basgeng  13585  epttop  13593  ntrin  13627  isopn3  13628  neiuni  13664  tgrest  13672  resttopon  13674  rest0  13682  txdis  13780  hmeontr  13816  xmettx  14013  findset  14700  pwtrufal  14750  pwf1oexmid  14752