Metamath Proof Explorer


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 V A tarskiMap A

Proof

Step Hyp Ref Expression
1 id A x A x
2 1 rgenw x Tarski A x A x
3 elintrabg A V A x Tarski | A x x Tarski A x A x
4 2 3 mpbiri A V A x Tarski | A x
5 tskmval A V tarskiMap A = x Tarski | A x
6 4 5 eleqtrrd A V A tarskiMap A