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?