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

Theorem grupw 9121
 Description: A Grothendieck universe contains the powerset of each of its members. (Contributed by Mario Carneiro, 9-Jun-2013.)
Assertion
Ref Expression
grupw

Proof of Theorem grupw
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elgrug 9118 . . . . 5
21ibi 241 . . . 4
32simprd 461 . . 3
4 simp1 995 . . . 4
54ralimi 2794 . . 3
6 pweq 3955 . . . . 5
76eleq1d 2469 . . . 4
87rspccv 3154 . . 3
93, 5, 83syl 20 . 2
109imp 427 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 367   w3a 972   wceq 1403   wcel 1840  wral 2751  cpw 3952  cpr 3971  cuni 4188   wtr 4486   crn 4941  (class class class)co 6232   cmap 7375  cgru 9116 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 974  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3058  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-nul 3736  df-if 3883  df-pw 3954  df-sn 3970  df-pr 3972  df-op 3976  df-uni 4189  df-br 4393  df-tr 4487  df-iota 5487  df-fv 5531  df-ov 6235  df-gru 9117 This theorem is referenced by:  gruss  9122  grurn  9127  gruxp  9133  grumap  9134  gruwun  9139  intgru  9140  gruina  9144  grur1a  9145
 Copyright terms: Public domain W3C validator