Metamath Proof Explorer
Description: The predecessor class exists when A does. (Contributed by Scott
Fenton, 8-Feb-2011)
|
|
Ref |
Expression |
|
Hypothesis |
predasetex.1 |
|
|
Assertion |
predasetex |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
predasetex.1 |
|
2 |
|
df-pred |
|
3 |
1
|
inex1 |
|
4 |
2 3
|
eqeltri |
|