Theorem 2ax6eOLD

Description: Obsolete version of 2ax6e as of 3-Oct-2023. (Contributed by Wolf Lammen, 28-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	2ax6eOLD	$$⊢\exists z\exists w\left(z=x\wedge w=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		aeveq	$$⊢\forall ww=z\to z=x$$
2		aeveq	$$⊢\forall ww=z\to w=y$$
3	1 2	jca	$$⊢\forall ww=z\to \left(z=x\wedge w=y\right)$$
4		19.8a	$$⊢\left(z=x\wedge w=y\right)\to \exists w\left(z=x\wedge w=y\right)$$
5		19.8a	$$⊢\exists w\left(z=x\wedge w=y\right)\to \exists z\exists w\left(z=x\wedge w=y\right)$$
6	3 4 5	3syl	$$⊢\forall ww=z\to \exists z\exists w\left(z=x\wedge w=y\right)$$
7		2ax6elem	$$⊢\neg \forall ww=z\to \exists z\exists w\left(z=x\wedge w=y\right)$$
8	6 7	pm2.61i	$$⊢\exists z\exists w\left(z=x\wedge w=y\right)$$