Theorem pwexg 2741

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 2399	. . 3 |- (x = A -> P~x = P~A)
2	1	eleq1d 1537	. 2 |- (x = A -> (P~x e. V <-> P~A e. V))
3		visset 1809	. . 3 |- x e. V
4	3	pwex 2740	. 2 |- P~x e. V
5	2, 4	vtoclg 1843	1 |- (A e. B -> P~A e. V)

Syntax hints:   -> wi 3   = wceq 954   e. wcel 956  Vcvv 1807  P~cpw 2397

This theorem is referenced by:  abssexg 2742  pwel 2754  uniexb 2902  xpexg 3254  fabexg 3644  mapex 4318  canth3 4830  istps3 7558  ntrfval 7617  clsfval 7618  neifval 7664  lpfval 7692  lmfval 7877  spwval2 8595  fiv 10410  qusp 10466  fgsb 10480  fgsb2 10485  efilcp2 10486

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047  df-ss 2049  df-pw 2398

Copyright terms: Public domain