Metamath Proof Explorer


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 x x = y z x

Proof

Step Hyp Ref Expression
1 el x z x
2 ax-1 z x x = y z x
3 1 2 eximii x x = y z x