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

Metamath Proof Explorer

Definition df-goex

Description: Define the Godel-set of existential quantification. Here N e.om corresponds to vN , and U represents another formula, and this expression is [ E. x ph ] = E.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-goex 
|- E.g N U = -.g A.g N -.g U

Detailed syntax breakdown

Step Hyp Ref Expression
0 cN 
 |-  N
1 cU 
 |-  U
2 1 0 cgox 
 |-  E.g N U
3 1 cgon 
 |-  -.g U
4 3 0 cgol 
 |-  A.g N -.g U
5 4 cgon 
 |-  -.g A.g N -.g U
6 2 5 wceq 
 |-  E.g N U = -.g A.g N -.g U