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 3479 . . . . 5 𝑦 ∈ V
21elintrab 4965 . . . 4 (𝑦 {𝑥𝐵𝐴𝑥} ↔ ∀𝑥𝐵 (𝐴𝑥𝑦𝑥))
3 ssid 4005 . . . . 5 𝐴𝐴
4 sseq2 4009 . . . . . . 7 (𝑥 = 𝐴 → (𝐴𝑥𝐴𝐴))
5 eleq2 2823 . . . . . . 7 (𝑥 = 𝐴 → (𝑦𝑥𝑦𝐴))
64, 5imbi12d 345 . . . . . 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 1542  wcel 2107  wral 3062  {crab 3433  wss 3949   cint 4951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-int 4952
This theorem is referenced by:  intmin2  4980  ordintdif  6415  uniordint  7789  onsucmin  7809  naddrid  8682  naddasslem1  8693  naddasslem2  8694  rankonidlem  9823  rankval4  9862  harsucnn  9993  mrcid  17557  lspid  20593  aspid  21429  cldcls  22546  spanid  30631  chsupid  30696  fldgenidfld  32438  igenidl2  36981  pclidN  38815  diaocN  40044  onuniintrab  42023  topclat  47671  toplatlub  47673  toplatjoin  47675
  Copyright terms: Public domain W3C validator