Description: A theorem about the universal class. Inference associated with bj-abv (which is proved from fewer axioms). (Contributed by Stefan Allan, 9-Dec-2008)
Ref | Expression | ||
---|---|---|---|
Hypothesis | sa-abvi.1 | |- ph |
|
Assertion | sa-abvi | |- _V = { x | ph } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sa-abvi.1 | |- ph |
|
2 | df-v | |- _V = { x | x = x } |
|
3 | equid | |- x = x |
|
4 | 3 1 | 2th | |- ( x = x <-> ph ) |
5 | 4 | abbii | |- { x | x = x } = { x | ph } |
6 | 2 5 | eqtri | |- _V = { x | ph } |