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

Theorem grothpwex 8704
 Description: Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth 8700. Note that ax-pow 4379 is not used by the proof. Use axpweq 4378 to obtain ax-pow 4379. (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 8701 . 2
2 simpl 445 . . . . . . . 8
32ralimi 2783 . . . . . . 7
4 pweq 3804 . . . . . . . . 9
54sseq1d 3377 . . . . . . . 8
65rspccv 3051 . . . . . . 7
73, 6syl 16 . . . . . 6
87anim2i 554 . . . . 5
983adant3 978 . . . 4
10 pm3.35 572 . . . 4
11 vex 2961 . . . . 5
1211ssex 4349 . . . 4
139, 10, 123syl 19 . . 3
1413exlimiv 1645 . 2
151, 14ax-mp 8 1
 Colors of variables: wff set class Syntax hints:   wi 4   wo 359   wa 360   w3a 937  wex 1551   wcel 1726  wral 2707  wrex 2708  cvv 2958   wss 3322  cpw 3801   class class class wbr 4214   cen 7108 This theorem is referenced by:  isrnsigaOLD  24497 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-groth 8700 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-v 2960  df-in 3329  df-ss 3336  df-pw 3803
 Copyright terms: Public domain W3C validator