Metamath Proof Explorer


Theorem ispointN

Description: The predicate "is a point". (Contributed by NM, 2-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses ispoint.a A = Atoms K
ispoint.p P = Points K
Assertion ispointN K D X P a A X = a

Proof

Step Hyp Ref Expression
1 ispoint.a A = Atoms K
2 ispoint.p P = Points K
3 1 2 pointsetN K D P = x | a A x = a
4 3 eleq2d K D X P X x | a A x = a
5 snex a V
6 eleq1 X = a X V a V
7 5 6 mpbiri X = a X V
8 7 rexlimivw a A X = a X V
9 eqeq1 x = X x = a X = a
10 9 rexbidv x = X a A x = a a A X = a
11 8 10 elab3 X x | a A x = a a A X = a
12 4 11 bitrdi K D X P a A X = a