Theorem intss1 1979

Description: An element of a class includes the intersection of the class. Exercise 4 of [TakeutiZaring] p. 44 (with correction), generalized to classes.

Assertion

Ref	Expression
intss1	|- (A e. B -> |^|B (_ A)

Proof of Theorem intss1

Step	Hyp	Ref	Expression
1		eleq1 1149	. . . . . 6 |- (y = A -> (y e. B <-> A e. B))
2		eleq2 1150	. . . . . 6 |- (y = A -> (x e. y <-> x e. A))
3	1, 2	imbi12d 474	. . . . 5 |- (y = A -> ((y e. B -> x e. y) <-> (A e. B -> x e. A)))
4	3	cla4gv 1396	. . . 4 |- (A e. B -> (A.y(y e. B -> x e. y) -> (A e. B -> x e. A)))
5	4	pm2.43a 60	. . 3 |- (A e. B -> (A.y(y e. B -> x e. y) -> x e. A))
6		visset 1350	. . . 4 |- x e. V
7	6	elint 1971	. . 3 |- (x e. |^|B <-> A.y(y e. B -> x e. y))
8	5, 7	syl5ib 181	. 2 |- (A e. B -> (x e. |^|B -> x e. A))
9	8	ssrdv 1509	1 |- (A e. B -> |^|B (_ A)

Syntax hints:   -> wi 2  A.wal 672   e. wel 803   = wceq 1091   e. wcel 1092   (_ wss 1487  |^|cint 1965

This theorem is referenced by:  int0el 1985  intex 1986  onint 2261  onssmin 2263  onintss 2266  onnmin 2270  oneqmini 2272  rankuni 3533  cardonle 3629  peano5nn 4424  shintcl 5294  ococint 5298  chsupsn 5313  shsumval2 5361

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-in 1491  df-ss 1492  df-int 1966

metamath.org