Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Andrew Salmon
Set Theory
ordpss
Next ⟩
fvsb
Metamath Proof Explorer
Ascii
Unicode
Theorem
ordpss
Description:
ordelpss
with an antecedent removed.
(Contributed by
Andrew Salmon
, 25-Jul-2011)
Ref
Expression
Assertion
ordpss
⊢
Ord
⁡
B
→
A
∈
B
→
A
⊂
B
Proof
Step
Hyp
Ref
Expression
1
ordelord
⊢
Ord
⁡
B
∧
A
∈
B
→
Ord
⁡
A
2
1
ex
⊢
Ord
⁡
B
→
A
∈
B
→
Ord
⁡
A
3
2
ancrd
⊢
Ord
⁡
B
→
A
∈
B
→
Ord
⁡
A
∧
A
∈
B
4
ordelpss
⊢
Ord
⁡
A
∧
Ord
⁡
B
→
A
∈
B
↔
A
⊂
B
5
4
ancoms
⊢
Ord
⁡
B
∧
Ord
⁡
A
→
A
∈
B
↔
A
⊂
B
6
5
biimpd
⊢
Ord
⁡
B
∧
Ord
⁡
A
→
A
∈
B
→
A
⊂
B
7
6
expimpd
⊢
Ord
⁡
B
→
Ord
⁡
A
∧
A
∈
B
→
A
⊂
B
8
3
7
syld
⊢
Ord
⁡
B
→
A
∈
B
→
A
⊂
B