Definition df-gobi

Description: Define the Godel-set of equivalence. Here the arguments U and V are also Godel-sets corresponding to smaller formulas. Note that this is aclass expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013)

	Ref	Expression
Assertion	df-gobi	⊢ ↔𝑔 = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( ( 𝑢 →𝑔 𝑣 ) ∧𝑔 ( 𝑣 →𝑔 𝑢 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgob	⊢ ↔𝑔
1		vu	⊢ 𝑢
2		cvv	⊢ V
3		vv	⊢ 𝑣
4	1	cv	⊢ 𝑢
5		cgoi	⊢ →𝑔
6	3	cv	⊢ 𝑣
7	4 6 5	co	⊢ ( 𝑢 →𝑔 𝑣 )
8		cgoa	⊢ ∧𝑔
9	6 4 5	co	⊢ ( 𝑣 →𝑔 𝑢 )
10	7 9 8	co	⊢ ( ( 𝑢 →𝑔 𝑣 ) ∧𝑔 ( 𝑣 →𝑔 𝑢 ) )
11	1 3 2 2 10	cmpo	⊢ ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( ( 𝑢 →𝑔 𝑣 ) ∧𝑔 ( 𝑣 →𝑔 𝑢 ) ) )
12	0 11	wceq	⊢ ↔𝑔 = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( ( 𝑢 →𝑔 𝑣 ) ∧𝑔 ( 𝑣 →𝑔 𝑢 ) ) )