Description: Demonstration of a theorem that requires the setvar variables x and
z to be disjoint (but without any other disjointness conditions, and
in particular, none on y ).

That theorem bundles the theorems ( |- E. x ( x = y -> z e. x ) with
x , y , z disjoint), often called its "principal instance", and the
two "degenerate instances" ( |- E. x ( x = x -> z e. x ) with
x , z disjoint) and ( |- E. x ( x = z -> z e. x ) with x , z
disjoint).

Compare with dvdemo1 , which has the same principal instance and one
common degenerate instance but crucially differs in the other degenerate
instance.

Note that dvdemo2 is partially bundled, in that the pairs of setvar
variables x , y and y , z need not be disjoint, and in spite of
that, its proof does not require any of the auxiliary axioms ax-10 ,
ax-11 , ax-12 , ax-13 . (Contributed by NM, 1-Dec-2006)(Revised by BJ, 13-Jan-2024)