Theorem dfsb7OLDOLD

Description: Obsolete version of dfsb7 as of 8-Jul-2023.

An alternate definition of proper substitution df-sb . By introducing a dummy variable z in the definiens, we are able to eliminate any distinct variable restrictions among the variables x , y , and ph of the definiendum. No distinct variable conflicts arise because z effectively insulates x from y . To achieve this, we use a chain of two substitutions in the form of sb5 , first z for x then y for z . Compare Definition 2.1'' of Quine p. 17, which is obtained from this theorem by applying df-clab . Theorem sb7h provides a version where ph and z don't have to be distinct. (Contributed by NM, 28-Jan-2004) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	dfsb7OLDOLD	$$⊢\left[y/x\right]\phi \leftrightarrow \exists z\left(z=y\wedge \exists x\left(x=z\wedge \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎz\phi$$
2	1	sb7f	$$⊢\left[y/x\right]\phi \leftrightarrow \exists z\left(z=y\wedge \exists x\left(x=z\wedge \phi \right)\right)$$