Theorem intmin 3237

Description: Any member of a class is the smallest of those members that include it. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)

Assertion

Ref	Expression
intmin	|- (A e. B -> |^|{x e. B | A C_ x} = A)

Distinct variable groups:   x,A   x,B

Proof of Theorem intmin

Step	Hyp	Ref	Expression
1		ssid 2634	. . . . 5 |- A C_ A
2		sseq2 2639	. . . . . . 7 |- (x = A -> (A C_ x <-> A C_ A))
3		eleq2 1958	. . . . . . 7 |- (x = A -> (y e. x <-> y e. A))
4	2, 3	imbi12d 688	. . . . . 6 |- (x = A -> ((A C_ x -> y e. x) <-> (A C_ A -> y e. A)))
5	4	rcla4v 2376	. . . . 5 |- (A e. B -> (A.x e. B (A C_ x -> y e. x) -> (A C_ A -> y e. A)))
6	1, 5	mpii 56	. . . 4 |- (A e. B -> (A.x e. B (A C_ x -> y e. x) -> y e. A))
7		visset 2295	. . . . 5 |- y e. _V
8	7	elintrab 3228	. . . 4 |- (y e. |^|{x e. B | A C_ x} <-> A.x e. B (A C_ x -> y e. x))
9	6, 8	syl5ib 223	. . 3 |- (A e. B -> (y e. |^|{x e. B | A C_ x} -> y e. A))
10	9	ssrdv 2622	. 2 |- (A e. B -> |^|{x e. B | A C_ x} C_ A)
11		ssintub 3235	. . 3 |- A C_ |^|{x e. B | A C_ x}
12	11	a1i 8	. 2 |- (A e. B -> A C_ |^|{x e. B | A C_ x})
13	10, 12	eqssd 2633	1 |- (A e. B -> |^|{x e. B | A C_ x} = A)

Syntax hints:   -> wi 3   = wceq 1298   e. wcel 1300  A.wral 2105  {crab 2108   C_ wss 2593  |^|cint 3214

This theorem is referenced by:  intmin2 3244  bm2.5ii 3887  onsucmin 3901  rankonid 5806  rankr1id 5808  rankval4 5813  cldcls 8958  chsupid 10944  spanid 10950  igenidl2 16213  ordintdif 16440

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-rab 2112  df-v 2294  df-in 2603  df-ss 2605  df-int 3215

Copyright terms: Public domain