Theorem sb56OLD

Description: Obsolete version of sbalex as of 21-Sep-2024. 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 nonfreeness 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) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sb56OLD	$$⊢\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)$$