Metamath Proof Explorer


Theorem ustelimasn

Description: Any point A is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017)

Ref Expression
Assertion ustelimasn U UnifOn X V U A X A V A

Proof

Step Hyp Ref Expression
1 simp3 U UnifOn X V U A X A X
2 ustdiag U UnifOn X V U I X V
3 2 3adant3 U UnifOn X V U A X I X V
4 opelidres A X A A I X A X
5 4 ibir A X A A I X
6 5 3ad2ant3 U UnifOn X V U A X A A I X
7 3 6 sseldd U UnifOn X V U A X A A V
8 elimasng A X A X A V A A A V
9 8 anidms A X A V A A A V
10 9 biimpar A X A A V A V A
11 1 7 10 syl2anc U UnifOn X V U A X A V A