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 
|- ( A e. B -> ( A e/ B -> ph ) )

Proof

Step Hyp Ref Expression
1 df-nel 
 |-  ( A e/ B <-> -. A e. B )
2 pm2.24 
 |-  ( A e. B -> ( -. A e. B -> ph ) )
3 1 2 syl5bi 
 |-  ( A e. B -> ( A e/ B -> ph ) )