Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-elpwg Structured version   Visualization version   GIF version

Theorem bj-elpwg 36237
Description: If the intersection of two classes is a set, then inclusion among these classes is equivalent to membership in the powerclass. Common generalization of elpwg 4605 and elpw2g 5344 (the latter of which could be proved from it). (Contributed by BJ, 31-Dec-2023.)
Assertion
Ref Expression
bj-elpwg ((𝐴𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))

Proof of Theorem bj-elpwg
StepHypRef Expression
1 elpwi 4609 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
2 ssidd 4005 . . . . . 6 (𝐴𝐵𝐴𝐴)
3 id 22 . . . . . 6 (𝐴𝐵𝐴𝐵)
42, 3ssind 4232 . . . . 5 (𝐴𝐵𝐴 ⊆ (𝐴𝐵))
5 ssexg 5323 . . . . 5 ((𝐴 ⊆ (𝐴𝐵) ∧ (𝐴𝐵) ∈ 𝑉) → 𝐴 ∈ V)
64, 5sylan 579 . . . 4 ((𝐴𝐵 ∧ (𝐴𝐵) ∈ 𝑉) → 𝐴 ∈ V)
7 elpwg 4605 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
87biimparc 479 . . . 4 ((𝐴𝐵𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
96, 8syldan 590 . . 3 ((𝐴𝐵 ∧ (𝐴𝐵) ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
109expcom 413 . 2 ((𝐴𝐵) ∈ 𝑉 → (𝐴𝐵𝐴 ∈ 𝒫 𝐵))
111, 10impbid2 225 1 ((𝐴𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2105  Vcvv 3473  cin 3947  wss 3948  𝒫 cpw 4602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-in 3955  df-ss 3965  df-pw 4604
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator