Theorem brrpss

Description: The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Hypothesis	brrpss.a	⊢ 𝐵 ∈ V
Assertion	brrpss	⊢ ( 𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		brrpss.a	⊢ 𝐵 ∈ V
2		brrpssg	⊢ ( 𝐵 ∈ V → ( 𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵 ) )
3	1 2	ax-mp	⊢ ( 𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵 )