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 34848
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 4491 and elpw2g 5212 (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 4497 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
2 ssidd 3900 . . . . . 6 (𝐴𝐵𝐴𝐴)
3 id 22 . . . . . 6 (𝐴𝐵𝐴𝐵)
42, 3ssind 4123 . . . . 5 (𝐴𝐵𝐴 ⊆ (𝐴𝐵))
5 ssexg 5191 . . . . 5 ((𝐴 ⊆ (𝐴𝐵) ∧ (𝐴𝐵) ∈ 𝑉) → 𝐴 ∈ V)
64, 5sylan 583 . . . 4 ((𝐴𝐵 ∧ (𝐴𝐵) ∈ 𝑉) → 𝐴 ∈ V)
7 elpwg 4491 . . . . 5 (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
87biimparc 483 . . . 4 ((𝐴𝐵𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
96, 8syldan 594 . . 3 ((𝐴𝐵 ∧ (𝐴𝐵) ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
109expcom 417 . 2 ((𝐴𝐵) ∈ 𝑉 → (𝐴𝐵𝐴 ∈ 𝒫 𝐵))
111, 10impbid2 229 1 ((𝐴𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wcel 2114  Vcvv 3398  cin 3842  wss 3843  𝒫 cpw 4488
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710  ax-sep 5167
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-rab 3062  df-v 3400  df-in 3850  df-ss 3860  df-pw 4490
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator