Set-theoretic tautologies Let us consider unquantifed formulas of a set theory (for example, NBG), more precisely,
the formulas, constructed from variables and the constants $\emptyset, V$ (the empty set 
and the class of all sets respectively), using only the following set-theoretic symbols:
$\cup, \cap, C, \subseteq, =$ (union, intersection, complement, inclusion, eqaulity, respectively).  
For any such formula F, not containing propositional connectives, the following very simple decision procedure (VSDP) can be used:
Let us denote as Prop(F) the result of replacement in F the symbols $\cup, \cap, C, \subseteq,\emptyset, V, =$
on the symbols $\vee, \wedge, \neg, \rightarrow, \equiv, false, true$, respectively.
Then the formula F is a (set-theoretic) tautology iff the formuala Prop(F) is a propositional tautology.
For example, the formula $X \subseteq X \cup Y$ is a set-theoretic tautology, 
because the formula Prop$(X \subseteq X \cup Y)$, that is, $X \rightarrow X \vee Y$ is a propositional tautology.
But this decision procedure (VSDP) works also for some unquantifed formulas, containing also 
in addition to the symbols $\cup, \cap, C, \subseteq, =$, also some propositional connectives.
For example, the formula $(X \subseteq X_1) \wedge (Y \subseteq Y_1) \rightarrow X \cup Y \subseteq X_1 \cup Y_1$
is  a set-theoretic tautology, and the formula 
$(X \rightarrow X_1) \wedge (Y \rightarrow Y_1) \rightarrow (X \vee Y) \rightarrow (X_1 \vee Y_1)$ 
is a propositional tautology.
So my question is:
What is the widest class of such formulas, for which this very simple decision procedure (VSDP) can be applied?
 A: $\DeclareMathOperator\pr{Prop}\let\sset\subseteq\let\nsset\nsubseteq$First, if $F$ is any valid quantifier-free formula, then $\pr(F)$ is a tautology: given a propositional assignment $e$ such that $e(\pr(F))=0$, the valuation
$$v(X)=\begin{cases}\varnothing&e(X)=0,\\V&e(X)=1\end{cases}$$
is a counter-example to $F$. Thus, the problem is what general conditions guarantee that when $\pr(F)$ is valid, $F$ is valid.
Without further clarification what counts as a “class” of formulas, the only possible answer is that this holds if and only it holds. (Valid quantifier-free formulas and propositional tautologies are both coNP-complete, incidentally.)
The formula $X\sset Y\lor Y\sset X$ is not valid, but its propositional translation, $(X\to Y)\lor(Y\to X)$, is. Note that this formula is a clause consisting of two positive literals.
On the other hand, the translation works faithfully for Horn formulas (conjunctions of clauses each of which contains at most one positive literal). It suffices to show this for Horn clauses
$$\tag{$*$}T_1(\vec X)\nsset T'_1(\vec X)\lor\cdots\lor T_n(\vec X)\nsset T'_n(\vec X)\lor T_0(\vec X)\sset T'_0(\vec X),$$
where $T_i,T'_i$ are Boolean terms in class variables $X_j$, and the last disjunct may be missing. If $(*)$ is not valid, fix a valuation to $\vec X$ that refutes it. Then $T_i(\vec X)\sset T'_i(\vec X)$ for all $i>0$, but $T_0(\vec X)\nsset T'_0(\vec X)$. Fix an element $a\in T_0(\vec X)$ such that $a\notin T'_0(\vec X)$. (If the $T_0\sset T'_0$ is missing in $(*)$, we can take $a$ arbitrary.) Define a propositional assignment
$$e(X_j)=\begin{cases}0&a\notin X_j\\1&a\in X_j\end{cases}.$$
Then the same expression holds also for arbitrary Boolean terms $T$ in place of $X_j$, hence $e(T_i\to T'_i)=1$ for all $i>0$, but $e(T_0\to T'_0)=0$. Thus, the propositional translation of $(*)$ is false under $e$.
The $X\sset Y\lor Y\sset X$ example above (which obviously generalizes to longer clauses with at least two positive literals) shows that as long as we restrict attention to classes of formulas defined by the shape of the outer propositional skeleton of the formula ignoring what is inside the atomic inclusions, Horn formulas are best possible.
EDIT: Let me add a higher-level explanation. The set of valid formulas of the form considered in the question is, up to trivial differences in notation, the universal theory of the “powerset” Boolean algebra of all classes, which is easily seen to coincide with the universal theory of all nontrivial Boolean algebras (or: all finite[ly generated] nontrivial Boolean algebras). On the other hand, $\pr(F)$ is a tautology iff $F$ holds in the 2-element Boolean algebra $\mathbf2$. Now, $\mathbf2$ generates Boolean algebras as a quasivariety, and more precisely, it generates all nontrivial Boolean algebras using subalgebras and nonempty direct products. Up to logical equivalence, universal Horn sentences are exactly the class of sentences preserved under subalgebras and nonempty direct products.
