Theorem bj-elpwg 34469

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 4500 and elpw2g 5211 (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

Step	Hyp	Ref	Expression
1		elpwi 4506	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssidd 3938	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ 𝐴)
3		id 22	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ 𝐵)
4	2, 3	ssind 4159	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐴 ∩ 𝐵))
5		ssexg 5191	. . . . 5 ⊢ ((𝐴 ⊆ (𝐴 ∩ 𝐵) ∧ (𝐴 ∩ 𝐵) ∈ 𝑉) → 𝐴 ∈ V)
6	4, 5	sylan 583	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐵) ∈ 𝑉) → 𝐴 ∈ V)
7		elpwg 4500	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
8	7	biimparc 483	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
9	6, 8	syldan 594	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐵) ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
10	9	expcom 417	. 2 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
11	1, 10	impbid2 229	1 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2111  Vcvv 3441   ∩ cin 3880   ⊆ wss 3881  𝒫 cpw 4497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by: (None)