Metamath Proof Explorer


Theorem grothpwex

Description: Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth . Note that ax-pow is not used by the proof. Use axpweq to obtain ax-pow . Use pwex or pwexg instead. (Contributed by Gérard Lang, 22-Jun-2009) (New usage is discouraged.)

Ref Expression
Assertion grothpwex 𝒫 x V

Proof

Step Hyp Ref Expression
1 simpl 𝒫 z y w y 𝒫 z w 𝒫 z y
2 1 ralimi z y 𝒫 z y w y 𝒫 z w z y 𝒫 z y
3 pweq z = x 𝒫 z = 𝒫 x
4 3 sseq1d z = x 𝒫 z y 𝒫 x y
5 4 rspccv z y 𝒫 z y x y 𝒫 x y
6 2 5 syl z y 𝒫 z y w y 𝒫 z w x y 𝒫 x y
7 6 anim2i x y z y 𝒫 z y w y 𝒫 z w x y x y 𝒫 x y
8 7 3adant3 x y z y 𝒫 z y w y 𝒫 z w z 𝒫 y z y z y x y x y 𝒫 x y
9 pm3.35 x y x y 𝒫 x y 𝒫 x y
10 vex y V
11 10 ssex 𝒫 x y 𝒫 x V
12 8 9 11 3syl x y z y 𝒫 z y w y 𝒫 z w z 𝒫 y z y z y 𝒫 x V
13 axgroth5 y x y z y 𝒫 z y w y 𝒫 z w z 𝒫 y z y z y
14 12 13 exlimiiv 𝒫 x V