Metamath Proof Explorer


Theorem isat2

Description: The predicate "is an atom". ( elatcv0 analog.) (Contributed by NM, 18-Jun-2012)

Ref Expression
Hypotheses isatom.b B=BaseK
isatom.z 0˙=0.K
isatom.c C=K
isatom.a A=AtomsK
Assertion isat2 KDPBPA0˙CP

Proof

Step Hyp Ref Expression
1 isatom.b B=BaseK
2 isatom.z 0˙=0.K
3 isatom.c C=K
4 isatom.a A=AtomsK
5 1 2 3 4 isat KDPAPB0˙CP
6 5 baibd KDPBPA0˙CP