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 36236
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 4604 and elpw2g 5343 (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 4608 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
2 ssidd 4004 . . . . . 6 (𝐴𝐵𝐴𝐴)
3 id 22 . . . . . 6 (𝐴𝐵𝐴𝐵)
42, 3ssind 4231 . . . . 5 (𝐴𝐵𝐴 ⊆ (𝐴𝐵))
5 ssexg 5322 . . . . 5 ((𝐴 ⊆ (𝐴𝐵) ∧ (𝐴𝐵) ∈ 𝑉) → 𝐴 ∈ V)
64, 5sylan 578 . . . 4 ((𝐴𝐵 ∧ (𝐴𝐵) ∈ 𝑉) → 𝐴 ∈ V)
7 elpwg 4604 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
87biimparc 478 . . . 4 ((𝐴𝐵𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
96, 8syldan 589 . . 3 ((𝐴𝐵 ∧ (𝐴𝐵) ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
109expcom 412 . 2 ((𝐴𝐵) ∈ 𝑉 → (𝐴𝐵𝐴 ∈ 𝒫 𝐵))
111, 10impbid2 225 1 ((𝐴𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2104  Vcvv 3472  cin 3946  wss 3947  𝒫 cpw 4601
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-in 3954  df-ss 3964  df-pw 4603
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator