Metamath Proof Explorer


Definition df-gzext

Description: The Godel-set version of the Axiom of Extensionality. (Contributed by Mario Carneiro, 14-Jul-2013)

Ref Expression
Assertion df-gzext AxExt = 𝑔 2 𝑜 2 𝑜 𝑔 𝑔 2 𝑜 𝑔 1 𝑜 𝑔 = 𝑔 1 𝑜

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgze class AxExt
1 c2o class 2 𝑜
2 cgoe class 𝑔
3 c0 class
4 1 3 2 co class 2 𝑜 𝑔
5 cgob class 𝑔
6 c1o class 1 𝑜
7 1 6 2 co class 2 𝑜 𝑔 1 𝑜
8 4 7 5 co class 2 𝑜 𝑔 𝑔 2 𝑜 𝑔 1 𝑜
9 8 1 cgol class 𝑔 2 𝑜 2 𝑜 𝑔 𝑔 2 𝑜 𝑔 1 𝑜
10 cgoi class 𝑔
11 cgoq class = 𝑔
12 3 6 11 co class = 𝑔 1 𝑜
13 9 12 10 co class 𝑔 2 𝑜 2 𝑜 𝑔 𝑔 2 𝑜 𝑔 1 𝑜 𝑔 = 𝑔 1 𝑜
14 0 13 wceq wff AxExt = 𝑔 2 𝑜 2 𝑜 𝑔 𝑔 2 𝑜 𝑔 1 𝑜 𝑔 = 𝑔 1 𝑜