Theorem tskmid

Description: The set A is an element of the smallest Tarski class that contains A . CLASSES1 th. 5. (Contributed by FL, 30-Dec-2010) (Proof shortened by Mario Carneiro, 21-Sep-2014)

	Ref	Expression
Assertion	tskmid	$$⊢A\in V\to A\in \mathrm{tarskiMap}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A\in x\to A\in x$$
2	1	rgenw	$$⊢\forall x\in \mathrm{Tarski}\left(A\in x\to A\in x\right)$$
3		elintrabg	$$⊢A\in V\to \left(A\in \bigcap \left\{x\in \mathrm{Tarski}|A\in x\right\}\leftrightarrow \forall x\in \mathrm{Tarski}\left(A\in x\to A\in x\right)\right)$$
4	2 3	mpbiri	$$⊢A\in V\to A\in \bigcap \left\{x\in \mathrm{Tarski}|A\in x\right\}$$
5		tskmval	$$⊢A\in V\to \mathrm{tarskiMap}\left(A\right)=\bigcap \left\{x\in \mathrm{Tarski}|A\in x\right\}$$
6	4 5	eleqtrrd	$$⊢A\in V\to A\in \mathrm{tarskiMap}\left(A\right)$$