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	$$⊢{\leftrightarrow }_{𝑔}=\left(u\in \mathrm{V},v\in \mathrm{V}⟼\left(u{\to }_{𝑔}v\right){\wedge }_{𝑔}\left(v{\to }_{𝑔}u\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgob	$$class{\leftrightarrow }_{𝑔}$$
1		vu	$$setvaru$$
2		cvv	$$class\mathrm{V}$$
3		vv	$$setvarv$$
4	1	cv	$$setvaru$$
5		cgoi	$$class{\to }_{𝑔}$$
6	3	cv	$$setvarv$$
7	4 6 5	co	$$class\left(u{\to }_{𝑔}v\right)$$
8		cgoa	$$class{\wedge }_{𝑔}$$
9	6 4 5	co	$$class\left(v{\to }_{𝑔}u\right)$$
10	7 9 8	co	$$class\left(\left(u{\to }_{𝑔}v\right){\wedge }_{𝑔}\left(v{\to }_{𝑔}u\right)\right)$$
11	1 3 2 2 10	cmpo	$$class\left(u\in \mathrm{V},v\in \mathrm{V}⟼\left(u{\to }_{𝑔}v\right){\wedge }_{𝑔}\left(v{\to }_{𝑔}u\right)\right)$$
12	0 11	wceq	$$wff{\leftrightarrow }_{𝑔}=\left(u\in \mathrm{V},v\in \mathrm{V}⟼\left(u{\to }_{𝑔}v\right){\wedge }_{𝑔}\left(v{\to }_{𝑔}u\right)\right)$$