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	|- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )

Proof

Step	Hyp	Ref	Expression
1		ax6e2nd	|- ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )
2		ax6e2eq	|- ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
3	1	a1d	|- ( -. A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
4	2 3	pm2.61i	|- ( u = v -> E. x E. y ( x = u /\ y = v ) )
5	1 4	jaoi	|- ( ( -. A. x x = y \/ u = v ) -> E. x E. y ( x = u /\ y = v ) )
6		olc	|- ( u = v -> ( -. A. x x = y \/ u = v ) )
7	6	a1d	|- ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
8		excom	|- ( E. x E. y ( x = u /\ y = v ) <-> E. y E. x ( x = u /\ y = v ) )
9		neeq1	|- ( x = u -> ( x =/= v <-> u =/= v ) )
10	9	biimprcd	|- ( u =/= v -> ( x = u -> x =/= v ) )
11	10	adantrd	|- ( u =/= v -> ( ( x = u /\ y = v ) -> x =/= v ) )
12		simpr	|- ( ( x = u /\ y = v ) -> y = v )
13	12	a1i	|- ( u =/= v -> ( ( x = u /\ y = v ) -> y = v ) )
14		neeq2	|- ( y = v -> ( x =/= y <-> x =/= v ) )
15	14	biimprcd	|- ( x =/= v -> ( y = v -> x =/= y ) )
16	11 13 15	syl6c	|- ( u =/= v -> ( ( x = u /\ y = v ) -> x =/= y ) )
17		sp	|- ( A. x x = y -> x = y )
18	17	necon3ai	|- ( x =/= y -> -. A. x x = y )
19	16 18	syl6	|- ( u =/= v -> ( ( x = u /\ y = v ) -> -. A. x x = y ) )
20	19	eximdv	|- ( u =/= v -> ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) )
21		nfnae	|- F/ x -. A. x x = y
22	21	19.9	|- ( E. x -. A. x x = y <-> -. A. x x = y )
23	20 22	imbitrdi	|- ( u =/= v -> ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) )
24	23	eximdv	|- ( u =/= v -> ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) )
25	8 24	biimtrid	|- ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) )
26		nfnae	|- F/ y -. A. x x = y
27	26	19.9	|- ( E. y -. A. x x = y <-> -. A. x x = y )
28	25 27	imbitrdi	|- ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> -. A. x x = y ) )
29		orc	|- ( -. A. x x = y -> ( -. A. x x = y \/ u = v ) )
30	28 29	syl6	|- ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
31	7 30	pm2.61ine	|- ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) )
32	5 31	impbii	|- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )