Description: The Godel-set version of the Axiom of Extensionality. (Contributed by Mario Carneiro, 14-Jul-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | df-gzext |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cgze | ||
1 | c2o | ||
2 | cgoe | ||
3 | c0 | ||
4 | 1 3 2 | co | |
5 | cgob | ||
6 | c1o | ||
7 | 1 6 2 | co | |
8 | 4 7 5 | co | |
9 | 8 1 | cgol | |
10 | cgoi | ||
11 | cgoq | ||
12 | 3 6 11 | co | |
13 | 9 12 10 | co | |
14 | 0 13 | wceq |