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 = ( ∀𝑔 2o ( ( 2o ∈𝑔 ∅ ) ↔𝑔 ( 2o ∈𝑔 1o ) ) →𝑔 ( ∅ =𝑔 1o ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgze	⊢ AxExt
1		c2o	⊢ 2o
2		cgoe	⊢ ∈𝑔
3		c0	⊢ ∅
4	1 3 2	co	⊢ ( 2o ∈𝑔 ∅ )
5		cgob	⊢ ↔𝑔
6		c1o	⊢ 1o
7	1 6 2	co	⊢ ( 2o ∈𝑔 1o )
8	4 7 5	co	⊢ ( ( 2o ∈𝑔 ∅ ) ↔𝑔 ( 2o ∈𝑔 1o ) )
9	8 1	cgol	⊢ ∀𝑔 2o ( ( 2o ∈𝑔 ∅ ) ↔𝑔 ( 2o ∈𝑔 1o ) )
10		cgoi	⊢ →𝑔
11		cgoq	⊢ =𝑔
12	3 6 11	co	⊢ ( ∅ =𝑔 1o )
13	9 12 10	co	⊢ ( ∀𝑔 2o ( ( 2o ∈𝑔 ∅ ) ↔𝑔 ( 2o ∈𝑔 1o ) ) →𝑔 ( ∅ =𝑔 1o ) )
14	0 13	wceq	⊢ AxExt = ( ∀𝑔 2o ( ( 2o ∈𝑔 ∅ ) ↔𝑔 ( 2o ∈𝑔 1o ) ) →𝑔 ( ∅ =𝑔 1o ) )