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

Theorem intmin 4973
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 3476 . . . . 5 𝑦 ∈ V
21elintrab 4965 . . . 4 (𝑦 {𝑥𝐵𝐴𝑥} ↔ ∀𝑥𝐵 (𝐴𝑥𝑦𝑥))
3 ssid 4005 . . . . 5 𝐴𝐴
4 sseq2 4009 . . . . . . 7 (𝑥 = 𝐴 → (𝐴𝑥𝐴𝐴))
5 eleq2 2820 . . . . . . 7 (𝑥 = 𝐴 → (𝑦𝑥𝑦𝐴))
64, 5imbi12d 343 . . . . . 6 (𝑥 = 𝐴 → ((𝐴𝑥𝑦𝑥) ↔ (𝐴𝐴𝑦𝐴)))
76rspcv 3609 . . . . 5 (𝐴𝐵 → (∀𝑥𝐵 (𝐴𝑥𝑦𝑥) → (𝐴𝐴𝑦𝐴)))
83, 7mpii 46 . . . 4 (𝐴𝐵 → (∀𝑥𝐵 (𝐴𝑥𝑦𝑥) → 𝑦𝐴))
92, 8biimtrid 241 . . 3 (𝐴𝐵 → (𝑦 {𝑥𝐵𝐴𝑥} → 𝑦𝐴))
109ssrdv 3989 . 2 (𝐴𝐵 {𝑥𝐵𝐴𝑥} ⊆ 𝐴)
11 ssintub 4971 . . 3 𝐴 {𝑥𝐵𝐴𝑥}
1211a1i 11 . 2 (𝐴𝐵𝐴 {𝑥𝐵𝐴𝑥})
1310, 12eqssd 4000 1 (𝐴𝐵 {𝑥𝐵𝐴𝑥} = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wcel 2104  wral 3059  {crab 3430  wss 3949   cint 4951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-in 3956  df-ss 3966  df-int 4952
This theorem is referenced by:  intmin2  4980  ordintdif  6415  uniordint  7793  onsucmin  7813  naddrid  8686  naddasslem1  8697  naddasslem2  8698  rankonidlem  9827  rankval4  9866  harsucnn  9997  mrcid  17563  lspid  20739  aspid  21650  cldcls  22768  spanid  30865  chsupid  30930  fldgenidfld  32675  igenidl2  37238  pclidN  39072  diaocN  40301  onuniintrab  42279  topclat  47712  toplatlub  47714  toplatjoin  47716
  Copyright terms: Public domain W3C validator