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 e. V -> A e. ( tarskiMap ` A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | |- ( A e. x -> A e. x ) |
|
| 2 | 1 | rgenw | |- A. x e. Tarski ( A e. x -> A e. x ) |
| 3 | elintrabg | |- ( A e. V -> ( A e. |^| { x e. Tarski | A e. x } <-> A. x e. Tarski ( A e. x -> A e. x ) ) ) |
|
| 4 | 2 3 | mpbiri | |- ( A e. V -> A e. |^| { x e. Tarski | A e. x } ) |
| 5 | tskmval | |- ( A e. V -> ( tarskiMap ` A ) = |^| { x e. Tarski | A e. x } ) |
|
| 6 | 4 5 | eleqtrrd | |- ( A e. V -> A e. ( tarskiMap ` A ) ) |