Atomic forcing of check names

Induct on the sorted pair of membership ranks of x,y to compute equality. If $x=y$, given any entry $⟨\check{u},s⟩\in \check{x}$ and any $q\le p,s$, take the entry $⟨\check{u},q⟩\in \check{y}$ and r=q. The induction hypothesis gives $q⊩\check{u}=\check{u}$, since u is a member of both x and y and both ranks decreased. Thus both subset clauses hold at p. If $x\mathrm{\ne }y$, choose a member u of one of the two differences, say $u\in x\setminus y$. The entry $⟨\check{u},p⟩\in \check{x}$ and common extension q=p have no witness in $\check{y}$: every $v\in y$ differs from u, and the equality induction says no r forces $\check{u}=\check{v}$. The subset clause fails, hence so does equality. The other difference gives the symmetric failure. If both sets are empty the two subset clauses are vacuous, starting the induction.

Suppose $x\in y$. For any $q\le p$, the entry $⟨\check{x},q⟩\in \check{y}$ together with r=q is a membership witness: equality of $\check{x}$ with itself was proved in step 1.1 for every ground x and every condition. Hence p forces membership. If $x\mathrm{\notin }y$, every candidate $v\in y$ differs from x, so step 1.1 excludes its equality witness at every r. The membership witness set is empty and cannot be dense below p, since p itself has no refinement in it. Thus no condition forces membership.

These are exactly both biconditionals. For example, putting $x=\mathrm{\varnothing }$ and $y=\{\mathrm{\varnothing }\}$ gives forced membership and failed equality at every condition, while $x=y=\mathrm{\varnothing }$ gives forced equality and failed membership. The coefficient computations above use no maximal antichain, generic existence or AC.