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	⊢ ∃ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		elALT2	⊢ ∃ 𝑥 𝑧 ∈ 𝑥
2		ax-1	⊢ ( 𝑧 ∈ 𝑥 → ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 ) )
3	1 2	eximii	⊢ ∃ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 )