Theorem wl-lem-moexsb

Description: The antecedent A. x ( ph -> x = z ) relates to E* x ph , but is better suited for usage in proofs. Note that no distinct variable restriction is placed on ph .

This theorem provides a basic working step in proving theorems about E* or E! . (Contributed by Wolf Lammen, 3-Oct-2019)

	Ref	Expression
Assertion	wl-lem-moexsb	$$⊢\forall x\left(\phi \to x=z\right)\to \left(\exists x\phi \leftrightarrow \left[z/x\right]\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfa1	$$⊢Ⅎx\forall x\left(\phi \to x=z\right)$$
2		nfs1v	$$⊢Ⅎx\left[z/x\right]\phi$$
3		sp	$$⊢\forall x\left(\phi \to x=z\right)\to \left(\phi \to x=z\right)$$
4		ax12v2	$$⊢x=z\to \left(\phi \to \forall x\left(x=z\to \phi \right)\right)$$
5	3 4	syli	$$⊢\forall x\left(\phi \to x=z\right)\to \left(\phi \to \forall x\left(x=z\to \phi \right)\right)$$
6		sb6	$$⊢\left[z/x\right]\phi \leftrightarrow \forall x\left(x=z\to \phi \right)$$
7	5 6	syl6ibr	$$⊢\forall x\left(\phi \to x=z\right)\to \left(\phi \to \left[z/x\right]\phi \right)$$
8	1 2 7	exlimd	$$⊢\forall x\left(\phi \to x=z\right)\to \left(\exists x\phi \to \left[z/x\right]\phi \right)$$
9		spsbe	$$⊢\left[z/x\right]\phi \to \exists x\phi$$
10	8 9	impbid1	$$⊢\forall x\left(\phi \to x=z\right)\to \left(\exists x\phi \leftrightarrow \left[z/x\right]\phi \right)$$