Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Proper subset relation
relrpss
Next ⟩
brrpssg
Metamath Proof Explorer
Ascii
Unicode
Theorem
relrpss
Description:
The proper subset relation is a relation.
(Contributed by
Stefan O'Rear
, 2-Nov-2014)
Ref
Expression
Assertion
relrpss
⊢
Rel
⁡
[⊂]
Proof
Step
Hyp
Ref
Expression
1
df-rpss
⊢
[⊂]
=
x
y
|
x
⊂
y
2
1
relopabiv
⊢
Rel
⁡
[⊂]