Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  grothpwex Unicode version

Theorem grothpwex 8449
 Description: Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth 8445. Note that ax-pow 4188 is not used by the proof. Use axpweq 4187 to obtain ax-pow 4188. (Contributed by Gérard Lang, 22-Jun-2009.)
Assertion
Ref Expression
grothpwex

Proof of Theorem grothpwex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axgroth5 8446 . 2
2 simpl 443 . . . . . . . 8
32ralimi 2618 . . . . . . 7
4 pweq 3628 . . . . . . . . 9
54sseq1d 3205 . . . . . . . 8
65rspccv 2881 . . . . . . 7
73, 6syl 15 . . . . . 6
87anim2i 552 . . . . 5
983adant3 975 . . . 4
10 pm3.35 570 . . . 4
11 vex 2791 . . . . 5
1211ssex 4158 . . . 4
139, 10, 123syl 18 . . 3
1413exlimiv 1666 . 2
151, 14ax-mp 8 1
 Colors of variables: wff set class Syntax hints:   wi 4   wo 357   wa 358   w3a 934  wex 1528   wceq 1623   wcel 1684  wral 2543  wrex 2544  cvv 2788   wss 3152  cpw 3625   class class class wbr 4023   cen 6860 This theorem is referenced by:  isrnsigaOLD  23473 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-groth 8445 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627
 Copyright terms: Public domain W3C validator