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	|- E. x ( x = y -> z e. x )

Proof

Step	Hyp	Ref	Expression
1		el	|- E. x z e. x
2		ax-1	|- ( z e. x -> ( x = y -> z e. x ) )
3	1 2	eximii	|- E. x ( x = y -> z e. x )