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
Structured
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
⊢
[
⊊
] = { 〈
𝑥
,
𝑦
〉 ∣
𝑥
⊊
𝑦
}
2
1
relopabiv
⊢
Rel [
⊊
]