ustelimasn

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

		Ref	Expression
	Assertion	ustelimasn	$⊢ (U \in UnifOn (X) \land V \in U \land A \in X) \to A \in V [\{A\}]$

Step	Hyp	Ref	Expression
1		simp3	$⊢ (U \in UnifOn (X) \land V \in U \land A \in X) \to A \in X$
2		ustdiag	$⊢ (U \in UnifOn (X) \land V \in U) \to {I ↾}_{X} \subseteq V$
3	2	3adant3	$⊢ (U \in UnifOn (X) \land V \in U \land A \in X) \to {I ↾}_{X} \subseteq V$
4		opelidres	$⊢ A \in X \to (⟨A, A⟩ \in ({I ↾}_{X}) \leftrightarrow A \in X)$
5	4	ibir	$⊢ A \in X \to ⟨A, A⟩ \in ({I ↾}_{X})$
6	5	3ad2ant3	$⊢ (U \in UnifOn (X) \land V \in U \land A \in X) \to ⟨A, A⟩ \in ({I ↾}_{X})$
7	3 6	sseldd	$⊢ (U \in UnifOn (X) \land V \in U \land A \in X) \to ⟨A, A⟩ \in V$
8		elimasng	$⊢ (A \in X \land A \in X) \to (A \in V [\{A\}] \leftrightarrow ⟨A, A⟩ \in V)$
9	8	anidms	$⊢ A \in X \to (A \in V [\{A\}] \leftrightarrow ⟨A, A⟩ \in V)$
10	9	biimpar	$⊢ (A \in X \land ⟨A, A⟩ \in V) \to A \in V [\{A\}]$
11	1 7 10	syl2anc	$⊢ (U \in UnifOn (X) \land V \in U \land A \in X) \to A \in V [\{A\}]$

Metamath Proof Explorer