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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | ||
2 | 1 | rgenw | |
3 | elintrabg | ||
4 | 2 3 | mpbiri | |
5 | tskmval | ||
6 | 4 5 | eleqtrrd |