Theorem pwexg 2752

Description: Power set axiom expressed in class notation, with the sethood requirement as an antecedent. Axiom 4 of [TakeutiZaring] p. 17.

Assertion

Ref	Expression
pwexg	|- (A e. B -> P~A e. V)

Proof of Theorem pwexg

Step	Hyp	Ref	Expression
1		pweq 2407	. . 3 |- (x = A -> P~x = P~A)
2	1	eleq1d 1543	. 2 |- (x = A -> (P~x e. V <-> P~A e. V))
3		visset 1816	. . 3 |- x e. V
4	3	pwex 2751	. 2 |- P~x e. V
5	2, 4	vtoclg 1850	1 |- (A e. B -> P~A e. V)

Syntax hints:   -> wi 3   = wceq 958   e. wcel 960  Vcvv 1814  P~cpw 2405

This theorem is referenced by:  abssexg 2753  pwel 2765  uniexb 2913  xpexg 3265  fabexg 3659  mapex 4334  canth3 4861  istps3 7609  ntrfval 7664  clsfval 7665  neifval 7711  lpfval 7739  lmfval 7922  spwval2 8649  fiv 10470  qusp 10541  fgsb 10555  fgsb2 10560  efilcp2 10561  rcfpfil 10569  sfvlim 10576  sfvlimOLD 10577

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-in 2054  df-ss 2056  df-pw 2406

Copyright terms: Public domain