Definition df-gzun

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

	Ref	Expression
Assertion	df-gzun	⊢ AxUn = ∃𝑔 1o ∀𝑔 2o ( ∃𝑔 1o ( ( 2o ∈𝑔 1o ) ∧𝑔 ( 1o ∈𝑔 ∅ ) ) →𝑔 ( 2o ∈𝑔 1o ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgzu	⊢ AxUn
1		c1o	⊢ 1o
2		c2o	⊢ 2o
3		cgoe	⊢ ∈𝑔
4	2 1 3	co	⊢ ( 2o ∈𝑔 1o )
5		cgoa	⊢ ∧𝑔
6		c0	⊢ ∅
7	1 6 3	co	⊢ ( 1o ∈𝑔 ∅ )
8	4 7 5	co	⊢ ( ( 2o ∈𝑔 1o ) ∧𝑔 ( 1o ∈𝑔 ∅ ) )
9	8 1	cgox	⊢ ∃𝑔 1o ( ( 2o ∈𝑔 1o ) ∧𝑔 ( 1o ∈𝑔 ∅ ) )
10		cgoi	⊢ →𝑔
11	9 4 10	co	⊢ ( ∃𝑔 1o ( ( 2o ∈𝑔 1o ) ∧𝑔 ( 1o ∈𝑔 ∅ ) ) →𝑔 ( 2o ∈𝑔 1o ) )
12	11 2	cgol	⊢ ∀𝑔 2o ( ∃𝑔 1o ( ( 2o ∈𝑔 1o ) ∧𝑔 ( 1o ∈𝑔 ∅ ) ) →𝑔 ( 2o ∈𝑔 1o ) )
13	12 1	cgox	⊢ ∃𝑔 1o ∀𝑔 2o ( ∃𝑔 1o ( ( 2o ∈𝑔 1o ) ∧𝑔 ( 1o ∈𝑔 ∅ ) ) →𝑔 ( 2o ∈𝑔 1o ) )
14	0 13	wceq	⊢ AxUn = ∃𝑔 1o ∀𝑔 2o ( ∃𝑔 1o ( ( 2o ∈𝑔 1o ) ∧𝑔 ( 1o ∈𝑔 ∅ ) ) →𝑔 ( 2o ∈𝑔 1o ) )