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 ∀𝑔 𝑁 𝑈 = ⟨ 2o , ⟨ 𝑁 , 𝑈 ⟩ ⟩

Detailed syntax breakdown

Step Hyp Ref Expression
0 cN ⊢ 𝑁
1 cU ⊢ 𝑈
2 1 0 cgol ⊢ ∀𝑔 𝑁 𝑈
3 c2o ⊢ 2o
4 0 1 cop ⊢ ⟨ 𝑁 , 𝑈 ⟩
5 3 4 cop ⊢ ⟨ 2o , ⟨ 𝑁 , 𝑈 ⟩ ⟩
6 2 5 wceq ⊢ ∀𝑔 𝑁 𝑈 = ⟨ 2o , ⟨ 𝑁 , 𝑈 ⟩ ⟩