Metamath Proof Explorer
Description: Nonempty class abstraction. See also ab0 . (Contributed by NM, 26-Dec-1996) (Proof shortened by Mario Carneiro, 11-Nov-2016)
|
|
Ref |
Expression |
|
Assertion |
abn0 |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
nfab1 |
|
2 |
1
|
n0f |
|
3 |
|
abid |
|
4 |
3
|
exbii |
|
5 |
2 4
|
bitri |
|