Theorem sseqin2 2281

Description: A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18.

Assertion

Ref	Expression
sseqin2	⊢ (A ⊆ B ↔ (B ∩ A) = A)

Proof of Theorem sseqin2

Step	Hyp	Ref	Expression
1		df-ss 2105	. 2 ⊢ (A ⊆ B ↔ (A ∩ B) = A)
2		incom 2260	. . 3 ⊢ (A ∩ B) = (B ∩ A)
3	2	eqeq1i 1525	. 2 ⊢ ((A ∩ B) = A ↔ (B ∩ A) = A)
4	1, 3	bitri 171	1 ⊢ (A ⊆ B ↔ (B ∩ A) = A)

Syntax hints:   ↔ wb 144   = wceq 992   ∩ cin 2098   ⊆ wss 2099

This theorem is referenced by:  dfss4 2294  onfr 3014  resabs1 3478  pw2en 4587  fiint 4703  cmcmlem 9810  pjvec 9919  pjocvec 9920  ssmd2 10520  mdslmd4i 10541  irredlem2 10600  irredlem3 10601  dmdbr7ati 10633  compsub 11488  filrn 11643  subspabs 11903  iccbnd 12082

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-in 2103  df-ss 2105

Copyright terms: Public domain