Metamath Proof Explorer


Theorem atex

Description: At least one atom exists. (Contributed by NM, 15-Jul-2012)

Ref Expression
Hypothesis atex.1 A = Atoms K
Assertion atex K HL A

Proof

Step Hyp Ref Expression
1 atex.1 A = Atoms K
2 1 hl2at K HL p A q A p q
3 df-rex p A q A p q p p A q A p q
4 exsimpl p p A q A p q p p A
5 3 4 sylbi p A q A p q p p A
6 2 5 syl K HL p p A
7 n0 A p p A
8 6 7 sylibr K HL A