Theorem intss1 2544

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 1532	. . . . . 6 |- (y = A -> (y e. B <-> A e. B))
2		eleq2 1533	. . . . . 6 |- (y = A -> (x e. y <-> x e. A))
3	1, 2	imbi12d 625	. . . . 5 |- (y = A -> ((y e. B -> x e. y) <-> (A e. B -> x e. A)))
4	3	cla4gv 1859	. . . 4 |- (A e. B -> (A.y(y e. B -> x e. y) -> (A e. B -> x e. A)))
5	4	pm2.43a 66	. . 3 |- (A e. B -> (A.y(y e. B -> x e. y) -> x e. A))
6		visset 1810	. . . 4 |- x e. V
7	6	elint 2535	. . 3 |- (x e. |^|B <-> A.y(y e. B -> x e. y))
8	5, 7	syl5ib 206	. 2 |- (A e. B -> (x e. |^|B -> x e. A))
9	8	ssrdv 2067	1 |- (A e. B -> |^|B (_ A)

Syntax hints:   -> wi 3  A.wal 953   = wceq 955   e. wcel 957   (_ wss 2044  |^|cint 2529

This theorem is referenced by:  intmin3 2554  intab 2556  int0el 2557  intex 2725  onint 3002  onssmin 3004  onintss 3007  onnmin 3011  oneqmini 3013  rankuni2 4673  cardonle 4805  peano5nn 5884  peano5uz 6161  shintcl 9248  ococint 9252  chsupsn 9267  shsumval2 9315

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-in 2048  df-ss 2050  df-int 2530

Copyright terms: Public domain