Theorem ssextss

Description: An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004)

	Ref	Expression
Assertion	ssextss	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		sspwb	⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵 )
2		df-ss	⊢ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) )
3		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
4		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵 )
5	3 4	imbi12i	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) ↔ ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) )
6	5	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) )
7	1 2 6	3bitri	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵 ) )