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	⊢ ∃_𝑔 𝑁 𝑈 = ¬_𝑔 ∀_𝑔 𝑁 ¬_𝑔 𝑈

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cN	⊢ 𝑁
1		cU	⊢ 𝑈
2	1 0	cgox	⊢ ∃_𝑔 𝑁 𝑈
3	1	cgon	⊢ ¬_𝑔 𝑈
4	3 0	cgol	⊢ ∀_𝑔 𝑁 ¬_𝑔 𝑈
5	4	cgon	⊢ ¬_𝑔 ∀_𝑔 𝑁 ¬_𝑔 𝑈
6	2 5	wceq	⊢ ∃_𝑔 𝑁 𝑈 = ¬_𝑔 ∀_𝑔 𝑁 ¬_𝑔 𝑈