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	|- <->g = ( u e. _V , v e. _V |-> ( ( u ->g v ) /\g ( v ->g u ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgob	|- <->g
1		vu	|- u
2		cvv	|- _V
3		vv	|- v
4	1	cv	|- u
5		cgoi	|- ->g
6	3	cv	|- v
7	4 6 5	co	|- ( u ->g v )
8		cgoa	|- /\g
9	6 4 5	co	|- ( v ->g u )
10	7 9 8	co	|- ( ( u ->g v ) /\g ( v ->g u ) )
11	1 3 2 2 10	cmpo	|- ( u e. _V , v e. _V |-> ( ( u ->g v ) /\g ( v ->g u ) ) )
12	0 11	wceq	|- <->g = ( u e. _V , v e. _V |-> ( ( u ->g v ) /\g ( v ->g u ) ) )