This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-goim

Description: Define the Godel-set of implication. 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-goim	$⊢ \to_{𝑔} = (u \in V, v \in V ⟼ u ⊼_{𝑔} [\neg_{𝑔} v])$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgoi	$class \to_{𝑔}$
1		vu	$setvar u$
2		cvv	$class V$
3		vv	$setvar v$
4	1	cv	$setvar u$
5		cgna	$class ⊼_{𝑔}$
6	3	cv	$setvar v$
7	6	cgon	$class [\neg_{𝑔} v]$
8	4 7 5	co	$class (u ⊼_{𝑔} [\neg_{𝑔} v])$
9	1 3 2 2 8	cmpo	$class (u \in V, v \in V ⟼ u ⊼_{𝑔} [\neg_{𝑔} v])$
10	0 9	wceq	$wff \to_{𝑔} = (u \in V, v \in V ⟼ u ⊼_{𝑔} [\neg_{𝑔} v])$