Theorem dvdemo2

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.

See https://us.metamath.org/mpeuni/mmset.html#distinct for details on the "disjoint variable" mechanism.

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)

	Ref	Expression
Assertion	dvdemo2	$$⊢\exists x\left(x=y\to z\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		elALT2	$$⊢\exists xz\in x$$
2		ax-1	$$⊢z\in x\to \left(x=y\to z\in x\right)$$
3	1 2	eximii	$$⊢\exists x\left(x=y\to z\in x\right)$$