Theorem elpwg 4570

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 5304. (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 3970	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵))
2		df-pw 4569	. 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵}
3	1, 2	elab2g 3648	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2149   ⊆ wss 3913  𝒫 cpw 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-pw 4569

This theorem is referenced by:  elpw  4571  elpwd  4573  elpwi  4574  elpwb  4575  pwidgOLD  4588  elpwunsn  4655  elpwdifsn  4761  prsspwg  4793  elpw2g  5304  snelpwg  5425  pwvrel  5712  eldifpw  7767  elpwun  7768  elpmg  8840  fopwdom  9073  elfpw  9311  rankwflemb  9765  r1elwf  9768  r1pw  9817  ackbij1lem3  10204  lcmfval  16679  lcmf0val  16680  acsfn  17715  evls1val  22449  evls1rhm  22451  evls1sca  22452  fiinopn  23027  clsval2  23176  ssntr  23184  neipeltop  23255  nrmsep3  23481  cnrmi  23486  cmpsublem  23525  conncompss  23559  kgeni  23663  ufileu  24045  filufint  24046  elutop  24359  ustuqtop0  24366  metustss  24677  psmetutop  24693  axtgcont1  28703  elpwincl1  32812  elpwdifcl  32813  elpwiuncl  32814  dispcmp  34194  sigaclci  34467  sigainb  34471  elsigagen2  34483  sigapildsys  34497  ldgenpisyslem1  34498  rossros  34515  measvunilem  34547  measdivcstALTV  34560  ddeval1  34569  ddeval0  34570  omsfval  34629  omssubaddlem  34634  omssubadd  34635  elcarsg  34640  limsucncmpi  36879  bj-elpwg  37610  topdifinffinlem  37915  elrels2  39014  ismrcd1  43355  elpwgded  45199  snelpwrVD  45465  elpwgdedVD  45551  sspwimpcf  45554  sspwimpcfVD  45555  sspwimpALT2  45562  pwpwuni  45703  dvnprodlem2  46587  ovolsplit  46628  stoweidlem50  46690  stoweidlem57  46697  pwsal  46955  salexct  46974  fsumlesge0  47017  psmeasurelem  47110  omessle  47138  caragensplit  47140  caragenelss  47141  omecl  47143  omeunile  47145  caragenuncl  47153  caragendifcl  47154  omeunle  47156  omeiunlempt  47160  carageniuncllem2  47162  carageniuncl  47163  0ome  47169  caragencmpl  47175  ovnval2  47185  ovncvrrp  47204  ovncl  47207  ovncvr2  47251  hspmbl  47269  isvonmbl  47278  smfresal  47428  stgredgel  48645  gsumlsscl  49079  lincfsuppcl  49112  linccl  49113  lincdifsn  49123  lincellss  49125  ellcoellss  49134  lindslinindimp2lem4  49160  lindslinindsimp2lem5  49161  lindslinindsimp2  49162  lincresunit3lem2  49179  opndisj  49600