Theorem sb56

Description: Two equivalent ways of expressing the proper substitution of y for x in ph , when x and y are distinct, namely, alternate definitions sb5 and sb6 . Theorem 6.2 of Quine p. 40. The proof does not involve df-sb . The implication "to the left" is equs4 and does not require any disjoint variable condition (but the version with a disjoint variable condition, equs4v , requires fewer axioms). Theorem equs45f replaces the disjoint variable condition with a non-freeness hypothesis and equs5 replaces it with a distinctor as antecedent. (Contributed by NM, 14-Apr-2008) Revised to use equsexv in place of equsex in order to remove dependency on ax-13 . (Revised by BJ, 20-Dec-2020)

	Ref	Expression
Assertion	sb56	$$⊢\exists x\left(x=y\wedge \phi \right)\leftrightarrow \forall x\left(x=y\to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sb5	$$⊢\left[y/x\right]\phi \leftrightarrow \exists x\left(x=y\wedge \phi \right)$$
2		sb6	$$⊢\left[y/x\right]\phi \leftrightarrow \forall x\left(x=y\to \phi \right)$$
3	1 2	bitr3i	$$⊢\exists x\left(x=y\wedge \phi \right)\leftrightarrow \forall x\left(x=y\to \phi \right)$$