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 = ( Base ` K )
isatom.z
|- .0. = ( 0. ` K )
isatom.c
|- C = ( 
isatom.a
|- A = ( Atoms ` K )
Assertion isat2
|- ( ( K e. D /\ P e. B ) -> ( P e. A <-> .0. C P ) )

Proof

Step Hyp Ref Expression
1 isatom.b
 |-  B = ( Base ` K )
2 isatom.z
 |-  .0. = ( 0. ` K )
3 isatom.c
 |-  C = ( 
4 isatom.a
 |-  A = ( Atoms ` K )
5 1 2 3 4 isat
 |-  ( K e. D -> ( P e. A <-> ( P e. B /\ .0. C P ) ) )
6 5 baibd
 |-  ( ( K e. D /\ P e. B ) -> ( P e. A <-> .0. C P ) )