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 𝑔 = u V , v V u 𝑔 ¬ 𝑔 v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgoi class 𝑔
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 ¬ 𝑔 v
8 4 7 5 co class u 𝑔 ¬ 𝑔 v
9 1 3 2 2 8 cmpo class u V , v V u 𝑔 ¬ 𝑔 v
10 0 9 wceq wff 𝑔 = u V , v V u 𝑔 ¬ 𝑔 v