Theorem elpwg 4603

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5333. (Contributed by NM, 6-Aug-2000.) (Proof shortened by BJ, 31-Dec-2023.)

Assertion

Ref	Expression
elpwg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Proof of Theorem elpwg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq1 4009	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵))
2		df-pw 4602	. 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵}
3	1, 2	elab2g 3680	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108   ⊆ wss 3951  𝒫 cpw 4600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-pw 4602

This theorem is referenced by:  elpw  4604  elpwd  4606  elpwi  4607  elpwb  4608  pwidg  4620  elpwunsn  4684  elpwdifsn  4789  prsspwg  4823  elpw2g  5333  snelpwg  5447  pwvrel  5735  eldifpw  7788  elpwun  7789  elpmg  8883  fopwdom  9120  elfpw  9394  rankwflemb  9833  r1elwf  9836  r1pw  9885  ackbij1lem3  10261  lcmfval  16658  lcmf0val  16659  acsfn  17702  evls1val  22324  evls1rhm  22326  evls1sca  22327  fiinopn  22907  clsval2  23058  ssntr  23066  neipeltop  23137  nrmsep3  23363  cnrmi  23368  cmpsublem  23407  conncompss  23441  kgeni  23545  ufileu  23927  filufint  23928  elutop  24242  ustuqtop0  24249  metustss  24564  psmetutop  24580  axtgcont1  28476  elpwincl1  32544  elpwdifcl  32545  elpwiuncl  32546  dispcmp  33858  sigaclci  34133  sigainb  34137  elsigagen2  34149  sigapildsys  34163  ldgenpisyslem1  34164  rossros  34181  measvunilem  34213  measdivcstALTV  34226  ddeval1  34235  ddeval0  34236  omsfval  34296  omssubaddlem  34301  omssubadd  34302  elcarsg  34307  limsucncmpi  36446  bj-elpwg  37053  topdifinffinlem  37348  elrels2  38487  ismrcd1  42709  elpwgded  44584  snelpwrVD  44851  elpwgdedVD  44937  sspwimpcf  44940  sspwimpcfVD  44941  sspwimpALT2  44948  pwpwuni  45062  dvnprodlem2  45962  ovolsplit  46003  stoweidlem50  46065  stoweidlem57  46072  pwsal  46330  salexct  46349  fsumlesge0  46392  psmeasurelem  46485  omessle  46513  caragensplit  46515  caragenelss  46516  omecl  46518  omeunile  46520  caragenuncl  46528  caragendifcl  46529  omeunle  46531  omeiunlempt  46535  carageniuncllem2  46537  carageniuncl  46538  0ome  46544  caragencmpl  46550  ovnval2  46560  ovncvrrp  46579  ovncl  46582  ovncvr2  46626  hspmbl  46644  isvonmbl  46653  smfresal  46803  stgredgel  47924  gsumlsscl  48296  lincfsuppcl  48330  linccl  48331  lincdifsn  48341  lincellss  48343  ellcoellss  48352  lindslinindimp2lem4  48378  lindslinindsimp2lem5  48379  lindslinindsimp2  48380  lincresunit3lem2  48397  opndisj  48800