Theorem bj-elpwg 37028

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 4556 and elpw2g 5275 (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 4560	. 2 ⊢ (𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
2		ssidd 3961	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ 𝐴)
3		id 22	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ 𝐵)
4	2, 3	ssind 4194	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ⊆ (𝐴 ∩ 𝐵))
5		ssexg 5265	. . . . 5 ⊢ ((𝐴 ⊆ (𝐴 ∩ 𝐵) ∧ (𝐴 ∩ 𝐵) ∈ 𝑉) → 𝐴 ∈ V)
6	4, 5	sylan 580	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐵) ∈ 𝑉) → 𝐴 ∈ V)
7		elpwg 4556	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
8	7	biimparc 479	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V) → 𝐴 ∈ 𝒫 𝐵)
9	6, 8	syldan 591	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐵) ∈ 𝑉) → 𝐴 ∈ 𝒫 𝐵)
10	9	expcom 413	. 2 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵))
11	1, 10	impbid2 226	1 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  Vcvv 3438   ∩ cin 3904   ⊆ wss 3905  𝒫 cpw 4553

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-in 3912  df-ss 3922  df-pw 4555

This theorem is referenced by: (None)