Theorem ax6e2ndeq

Description: "At least two sets exist" expressed in the form of dtru is logically equivalent to the same expressed in a form similar to ax6e if dtru is false implies u = v . ax6e2ndeq is derived from ax6e2ndeqVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ax6e2ndeq	$$⊢\left(\neg \forall xx=y\vee u=v\right)\leftrightarrow \exists x\exists y\left(x=u\wedge y=v\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax6e2nd	$$⊢\neg \forall xx=y\to \exists x\exists y\left(x=u\wedge y=v\right)$$
2		ax6e2eq	$$⊢\forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)$$
3	1	a1d	$$⊢\neg \forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)$$
4	2 3	pm2.61i	$$⊢u=v\to \exists x\exists y\left(x=u\wedge y=v\right)$$
5	1 4	jaoi	$$⊢\left(\neg \forall xx=y\vee u=v\right)\to \exists x\exists y\left(x=u\wedge y=v\right)$$
6		olc	$$⊢u=v\to \left(\neg \forall xx=y\vee u=v\right)$$
7	6	a1d	$$⊢u=v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)$$
8		excom	$$⊢\exists x\exists y\left(x=u\wedge y=v\right)\leftrightarrow \exists y\exists x\left(x=u\wedge y=v\right)$$
9		neeq1	$$⊢x=u\to \left(x\ne v\leftrightarrow u\ne v\right)$$
10	9	biimprcd	$$⊢u\ne v\to \left(x=u\to x\ne v\right)$$
11	10	adantrd	$$⊢u\ne v\to \left(\left(x=u\wedge y=v\right)\to x\ne v\right)$$
12		simpr	$$⊢\left(x=u\wedge y=v\right)\to y=v$$
13	12	a1i	$$⊢u\ne v\to \left(\left(x=u\wedge y=v\right)\to y=v\right)$$
14		neeq2	$$⊢y=v\to \left(x\ne y\leftrightarrow x\ne v\right)$$
15	14	biimprcd	$$⊢x\ne v\to \left(y=v\to x\ne y\right)$$
16	11 13 15	syl6c	$$⊢u\ne v\to \left(\left(x=u\wedge y=v\right)\to x\ne y\right)$$
17		sp	$$⊢\forall xx=y\to x=y$$
18	17	necon3ai	$$⊢x\ne y\to \neg \forall xx=y$$
19	16 18	syl6	$$⊢u\ne v\to \left(\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)$$
20	19	eximdv	$$⊢u\ne v\to \left(\exists x\left(x=u\wedge y=v\right)\to \exists x\neg \forall xx=y\right)$$
21		nfnae	$$⊢Ⅎx\neg \forall xx=y$$
22	21	19.9	$$⊢\exists x\neg \forall xx=y\leftrightarrow \neg \forall xx=y$$
23	20 22	syl6ib	$$⊢u\ne v\to \left(\exists x\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)$$
24	23	eximdv	$$⊢u\ne v\to \left(\exists y\exists x\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)$$
25	8 24	syl5bi	$$⊢u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)$$
26		nfnae	$$⊢Ⅎy\neg \forall xx=y$$
27	26	19.9	$$⊢\exists y\neg \forall xx=y\leftrightarrow \neg \forall xx=y$$
28	25 27	syl6ib	$$⊢u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)$$
29		orc	$$⊢\neg \forall xx=y\to \left(\neg \forall xx=y\vee u=v\right)$$
30	28 29	syl6	$$⊢u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)$$
31	7 30	pm2.61ine	$$⊢\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)$$
32	5 31	impbii	$$⊢\left(\neg \forall xx=y\vee u=v\right)\leftrightarrow \exists x\exists y\left(x=u\wedge y=v\right)$$