Theorem bj-elpwg

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 and elpw2g (the latter of which could be proved from it). (Contributed by BJ, 31-Dec-2023)

	Ref	Expression
Assertion	bj-elpwg	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elpwi	⊢ ( 𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵 )
2		ssidd	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ 𝐴 )
3		id	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ 𝐵 )
4	2 3	ssind	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ ( 𝐴 ∩ 𝐵 ) )
5		ssexg	⊢ ( ( 𝐴 ⊆ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ) → 𝐴 ∈ V )
6	4 5	sylan	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ) → 𝐴 ∈ V )
7		elpwg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )
8	7	biimparc	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ V ) → 𝐴 ∈ 𝒫 𝐵 )
9	6 8	syldan	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 ) → 𝐴 ∈ 𝒫 𝐵 )
10	9	expcom	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 → ( 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝒫 𝐵 ) )
11	1 10	impbid2	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )