Metamath Proof Explorer

Theorem elunnel1

Description: A member of a union that is not member of the first class, is member of the second class. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion elunnel1 A B C ¬ A B A C


Step Hyp Ref Expression
1 elun A B C A B A C
2 1 biimpi A B C A B A C
3 2 orcanai A B C ¬ A B A C