Metamath Proof Explorer


Theorem elnelall

Description: A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018)

Ref Expression
Assertion elnelall ABABφ

Proof

Step Hyp Ref Expression
1 df-nel AB¬AB
2 pm2.24 AB¬ABφ
3 1 2 syl5bi ABABφ