Theorem dvelim 2016

Description: This theorem can be used to eliminate a distinct variable restriction on x and z and replace it with the "distinctor" -. A.xx = y as an antecedent. ph normally has z free and can be read ph(z), and ps substitutes y for z and can be read ph(y). We don't require that x and y be distinct: if they aren't, the distinctor will become false (in multiple-element domains of discourse) and "protect" the consequent.

To obtain a closed-theorem form of this inference, prefix the hypotheses with A.xA.z, conjoin them, and apply dvelimdf 2082.

Other variants of this theorem are dvelimh 1964 (with no distinct variable restrictions), dvelimhw 1849 (that avoids ax-12 1925), and dvelimALT 2133 (that avoids ax-10 2140). (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
dvelim.1	|- (ph -> A.xph)
dvelim.2	|- (z = y -> (ph <-> ps))

Assertion

Ref	Expression
dvelim	|- (-. A.x x = y -> (ps -> A.xps))

Distinct variable group:   ps,z

Allowed substitution hints:   ph(x,y,z)   ps(x,y)

Proof of Theorem dvelim

Step	Hyp	Ref	Expression
1		dvelim.1	. 2 |- (ph -> A.xph)
2		ax-17 1616	. 2 |- (ps -> A.zps)
3		dvelim.2	. 2 |- (z = y -> (ph <-> ps))
4	1, 2, 3	dvelimh 1964	1 |- (-. A.x x = y -> (ps -> A.xps))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176  A.wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is referenced by:  ax15  2021  eujustALT  2207