MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  intmin Structured version   Visualization version   GIF version

Theorem intmin 4641
Description: Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Assertion
Ref Expression
intmin (𝐴𝐵 {𝑥𝐵𝐴𝑥} = 𝐴)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem intmin
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 vex 3335 . . . . 5 𝑦 ∈ V
21elintrab 4632 . . . 4 (𝑦 {𝑥𝐵𝐴𝑥} ↔ ∀𝑥𝐵 (𝐴𝑥𝑦𝑥))
3 ssid 3757 . . . . 5 𝐴𝐴
4 sseq2 3760 . . . . . . 7 (𝑥 = 𝐴 → (𝐴𝑥𝐴𝐴))
5 eleq2 2820 . . . . . . 7 (𝑥 = 𝐴 → (𝑦𝑥𝑦𝐴))
64, 5imbi12d 333 . . . . . 6 (𝑥 = 𝐴 → ((𝐴𝑥𝑦𝑥) ↔ (𝐴𝐴𝑦𝐴)))
76rspcv 3437 . . . . 5 (𝐴𝐵 → (∀𝑥𝐵 (𝐴𝑥𝑦𝑥) → (𝐴𝐴𝑦𝐴)))
83, 7mpii 46 . . . 4 (𝐴𝐵 → (∀𝑥𝐵 (𝐴𝑥𝑦𝑥) → 𝑦𝐴))
92, 8syl5bi 232 . . 3 (𝐴𝐵 → (𝑦 {𝑥𝐵𝐴𝑥} → 𝑦𝐴))
109ssrdv 3742 . 2 (𝐴𝐵 {𝑥𝐵𝐴𝑥} ⊆ 𝐴)
11 ssintub 4639 . . 3 𝐴 {𝑥𝐵𝐴𝑥}
1211a1i 11 . 2 (𝐴𝐵𝐴 {𝑥𝐵𝐴𝑥})
1310, 12eqssd 3753 1 (𝐴𝐵 {𝑥𝐵𝐴𝑥} = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1624  wcel 2131  wral 3042  {crab 3046  wss 3707   cint 4619
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rab 3051  df-v 3334  df-in 3714  df-ss 3721  df-int 4620
This theorem is referenced by:  intmin2  4648  ordintdif  5927  bm2.5ii  7163  onsucmin  7178  rankonidlem  8856  rankval4  8895  mrcid  16467  lspid  19176  aspid  19524  cldcls  21040  spanid  28507  chsupid  28572  igenidl2  34169  pclidN  35677  diaocN  36908
  Copyright terms: Public domain W3C validator