The proposition, an idea which may be judged
true or false, 𝛢. 

𝜑
𝐴 
𝛢 maps to proposition 𝜑 or class 𝐴.
V is the universal class of all sets.
∅ is the empty class.
Direct translation of a judgment into class notation requires
both the introduction of a dummy set variable and an assertion that
it has no unbound appearance in the class expression. Colloquially,
this is equivalent to saying it is equal to the class of all
sets. 
Proposition 𝛢 holds true. 

⊢ 𝜑
⊢ (Ⅎ𝑥𝐴 ∧ ∀𝑥𝑥 ∈ 𝐴)
⊢ 𝐴 = V 
The negation of proposition 𝛢. 

¬ 𝜑
(V ∖ 𝐴) 
Proposition 𝛢 holds false. 

⊢ ¬ 𝜑
⊢ (V ∖ 𝐴) = V
⊢ 𝐴 = ∅

The idea that 𝛣 implies 𝛢. 

(𝜑 → 𝜓)
((V ∖ 𝐵) ∪ 𝐴) 
𝛣 maps to 𝜑 or 𝐵.
𝛢 maps to 𝜓 or 𝐴.
Since Metamath's standard set.mm has more connectives for
propositions than just implication and negation, some of these
statements have fully equivalent synonyms. 
The judgment that the truth of 𝛣 implies
the truth of 𝛢. 

⊢ (𝜑 → 𝜓)
⊢ ((V ∖ 𝐵) ∪ 𝐴) = V
⊢ 𝐵 ⊆ 𝐴 
The judgment that not both 𝛣 and 𝛢
hold true. 

⊢ (𝜑 → ¬ 𝜓)
⊢ (𝜑 ⊼ 𝜓)
⊢ ((V ∖ 𝐵) ∪ (V ∖ 𝐴)) = V
⊢ (V ∖ (𝐵 ∩ 𝐴)) = V
⊢ (𝐵 ∩ 𝐴) = ∅
⊢ 𝐵 ⊆ (V ∖ 𝐴) 
The judgment that 𝛣 or 𝛢 (or
both) holds true. 

⊢ (¬ 𝜑 → 𝜓)
⊢ (𝜑 ∨ 𝜓)
⊢ (𝐵 ∪ 𝐴) = V
⊢ (V ∖ 𝐵) ⊆ 𝐴 
The judgment that both 𝛣 and 𝛢
hold true. 

⊢ ¬ (𝜑 → ¬ 𝜓)
⊢ ¬ (𝜑 ⊼ 𝜓)
⊢ (𝜑 ∧ 𝜓)
⊢ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐴))) = V
⊢ (V ∖ (V ∖ (𝐵 ∩ 𝐴))) = V
⊢ (𝐵 ∩ 𝐴) = V 
The judgment that exactly one of
𝛣 and 𝛢 holds true. 

⊢ ¬ ((¬ 𝜑 → 𝜓) → ¬ (𝜑 → ¬ 𝜓))
⊢ ((¬ 𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓))
⊢ (𝜑 ⊻ 𝜓)
⊢ ((𝐵 ∪ 𝐴) ∩ (V ∖ (𝐵 ∩ 𝐴))) = V
⊢ (V ∖ 𝐵) = 𝐴 

⊢ ¬ ((𝜑 → ¬ 𝜓) → ¬ (¬ 𝜑 → 𝜓))
⊢ ((𝜑 → ¬ 𝜓) ∧ (¬ 𝜑 → 𝜓))
⊢ (𝜑 ⊻ 𝜓)
⊢ ((V ∖ (𝐵 ∩ 𝐴)) ∩ (𝐵 ∪ 𝐴)) = V
⊢ 𝐵 = (V ∖ 𝐴) 
The judgment 𝛣 is true while
𝛢 is false. 

⊢ ¬ (𝜑 → 𝜓)
⊢ (𝜑 ∧ ¬ 𝜓)
⊢ (V ∖ ((V ∖ 𝐵) ∪ 𝐴)) = V
⊢ (𝐵 ∩ (V ∖ 𝐴)) = V
⊢ ((V ∖ 𝐵) ∪ 𝐴) = ∅ 

⊢ ¬ (¬ 𝜓 → ¬ 𝜑)
⊢ (¬ 𝜓 ∧ 𝜑)
⊢ (V ∖ (𝐴 ∪ (V ∖ 𝐵))) = V
⊢ ((V ∖ 𝐴) ∩ 𝐵) = V
⊢ (𝐴 ∪ (V ∖ 𝐵)) = ∅ 
The judgment that neither 𝛢 nor 𝛣
is true. 

⊢ ¬ (¬ 𝜓 → 𝜑)
⊢ ¬ (𝜓 ∨ 𝜑)
⊢ (V ∖ (𝐴 ∪ 𝐵)) = V
⊢ (𝐴 ∪ 𝐵) = ∅ 
The judgment that the truth of both 𝛤
and 𝛣 implies the truth of 𝛢. 

⊢ (𝜑 → (𝜓 → 𝜒))
⊢ ((𝜑 ∧ 𝜓) → 𝜒)
⊢ ((V ∖ 𝐶) ∪ ((V ∖ 𝐵) ∪ 𝐴)) = V
⊢ (((V ∖ 𝐶) ∪ (V ∖ 𝐵)) ∪ 𝐴) = V
⊢ ((V ∖ (𝐶 ∩ 𝐵)) ∪ 𝐴) = V
⊢ (𝐶 ∩ 𝐵) ⊆ 𝐴 
𝛤 maps to 𝜑 or 𝐶.
𝛣 maps to 𝜓 or 𝐵.
𝛢 maps to 𝜒 or 𝐴.
Since Metamath's standard set.mm has more connectives for
propositions than just implication and negation, some of these
statements have fully equivalent synonyms. 
The judgment that 𝛤, 𝛣, or
𝛢 (or any combination) holds true. 

⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒))
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒)
⊢ (𝜑 ∨ 𝜓 ∨ 𝜒)
⊢ (𝐶 ∪ (𝐵 ∪ 𝐴)) = V
⊢ ((𝐶 ∪ 𝐵) ∪ 𝐴) = V
⊢ (V / (𝐶 ∪ 𝐵)) ⊆ 𝐴 
The judgment that 𝛤, 𝛣, and
𝛢 all hold true. 

⊢ ¬ (𝜑 → (𝜓 → ¬ 𝜒))
⊢ ¬ ((𝜑 ∧ 𝜓) → ¬ 𝜒)
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)
⊢ (V ∖ ((V ∖ 𝐶) ∪ ((V ∖ 𝐵) ∪ (V ∖ 𝐴)))) = V
⊢ (𝐶 ∩ (𝐵 ∩ 𝐴)) = V
⊢ ((𝐶 ∩ 𝐵) ∩ 𝐴) = V 
The judgment that 𝛢 is equivalent to 𝛣. 

⊢ (𝜓 ↔ 𝜑)
⊢ {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜑}
⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
⊢ (((V ∖ 𝐴) ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐴)) = V
⊢ ((V ∖ (𝐴 ∪ 𝐵)) ∪ (𝐴 ∩ 𝐵)) = V
⊢ (𝐴 ∪ 𝐵) ⊆ (𝐴 ∩ 𝐵)
⊢ 𝐴 = 𝐵 
Fundamentally equality of classes can be distinguished from
logical equivalence, the equality of propositions, since classes are equal
if and only if they contain the same sets and not every class is a set. So
we have ⊢ ¬ (ω ⊆ 𝑋 ↔ (ω ⊆ 𝑋 ∧ 𝑋 ∈ V)) but
⊢ {𝑥 ∣ ω ⊆ 𝑥} = {𝑥 ∣ (ω ⊆ 𝑥 ∧ 𝑥 ∈ V)}. Thus
the assumption of naive set theory is where Frege must break down.
Intermediate between the two is when the strong condition of
biimplication implies the weaker equality of classes or relations
composed of sets which satisfy those propositions. With some
adaptation much can be salvaged by a forgiving translation.
𝛢 maps to 𝜓 or 𝐴.
𝛣 maps to 𝜑 or 𝐵 
The judgment that 𝛢 has the property
𝛷. (Which implies 𝛢 is a set.) 

⊢ [𝐴 / 𝑥]𝜑
⊢ 𝐴 ∈ 𝑃
⊢ 𝐴 ∈ {𝑥 ∣ 𝜑} 
𝛢 maps to 𝐴.
𝛣 maps to 𝐵.
𝛷 maps to 𝜑 or 𝑃 or {𝑥 ∣ 𝜑}.
𝛹 maps to 𝜓 or 𝑅 or {⟨𝑥, 𝑦⟩ ∣ 𝜓}.
𝔞 maps to 𝑎.
𝑥 and 𝑦 are distinct set variables which presumably,
but not necessarily, appear in what is eventually substituted for
𝜑 or 𝜓 and which nowhere appear in 𝐴 or 𝐵. 
The judgment that 𝛣 stands in relation
𝛹 to 𝛢. (Which implies that 𝛢 and 𝛣
are sets.) 

⊢ [𝐴 / 𝑥][𝐵 / 𝑦]𝜓
⊢ [𝐵 / 𝑦][𝐴 / 𝑥]𝜓
⊢ 𝐴𝑅𝐵
⊢ 𝐵^{◡}𝑅𝐴
⊢ 𝐴{⟨𝑥, 𝑦⟩ ∣ 𝜓}𝐵
⊢ 𝐴^{◡}{⟨𝑦, 𝑥⟩ ∣ 𝜓}𝐵
⊢ 𝐵{⟨𝑦, 𝑥⟩ ∣ 𝜓}𝐴
⊢ 𝐵^{◡}{⟨𝑥, 𝑦⟩ ∣ 𝜓}𝐴
⊢ 𝐵 ∈ (𝑅 “ {𝐴})
⊢ 𝐴 ∈ (^{◡}𝑅 “ {𝐵})
⊢ 𝐵 ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} “ {𝐴})
⊢ 𝐵 ∈ (^{◡}{⟨𝑦, 𝑥⟩ ∣ 𝜓} “ {𝐴})
⊢ 𝐴 ∈ (^{◡}{⟨𝑥, 𝑦⟩ ∣ 𝜓} “ {𝐵})
⊢ 𝐴 ∈ ({⟨𝑦, 𝑥⟩ ∣ 𝜓} “ {𝐵})

The judgment that all 𝔞 have the property
𝛷. 

⊢ ∀𝑎[𝑎 / 𝑥]𝜑
⊢ ∀𝑎𝑎 ∈ 𝑃
⊢ ∀𝑎𝑎 ∈ {𝑥 ∣ 𝜑} 
The negated judgment that no 𝔞 have the
property 𝛷. 

⊢ ¬ ∀𝑎¬ [𝑎 / 𝑥]𝜑
⊢ ∃𝑎[𝑎 / 𝑥]𝜑
⊢ ¬ ∀𝑎¬ 𝑎 ∈ 𝑃
⊢ ∃𝑎𝑎 ∈ 𝑃 