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

Metamath Proof Explorer

Definition df-goal

Description: Define the Godel-set of universal quantification. Here N e.om corresponds to vN , and U represents another formula, and this expression is [ A. x ph ] = A.g N U where x is the N -th variable, U = [ ph ] is the code for ph . Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013)

		Ref	Expression
	Assertion	df-goal	$⊢ [\forall_{𝑔} N U] = ⟨2_{𝑜}, ⟨N, U⟩⟩$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cN	$class N$
1		cU	$class U$
2	1 0	cgol	$class [\forall_{𝑔} N U]$
3		c2o	$class 2_{𝑜}$
4	0 1	cop	$class ⟨N, U⟩$
5	3 4	cop	$class ⟨2_{𝑜}, ⟨N, U⟩⟩$
6	2 5	wceq	$wff [\forall_{𝑔} N U] = ⟨2_{𝑜}, ⟨N, U⟩⟩$