Theorem ax6e2nd 43319

Description: If at least two sets exist (dtru 5437), then the same is true expressed in an alternate form similar to the form of ax6e 2383. ax6e2nd 43319 is derived from ax6e2ndVD 43669. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
ax6e2nd	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Distinct variable groups:   𝑥,𝑢   𝑦,𝑢   𝑥,𝑣

Proof of Theorem ax6e2nd

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3479	. . . . . . 7 ⊢ 𝑢 ∈ V
2		ax6e 2383	. . . . . . 7 ⊢ ∃𝑦 𝑦 = 𝑣
3	1, 2	pm3.2i 472	. . . . . 6 ⊢ (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣)
4		19.42v 1958	. . . . . . 7 ⊢ (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣))
5	4	biimpri 227	. . . . . 6 ⊢ ((𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣) → ∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣))
6	3, 5	ax-mp 5	. . . . 5 ⊢ ∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣)
7		isset 3488	. . . . . . 7 ⊢ (𝑢 ∈ V ↔ ∃𝑥 𝑥 = 𝑢)
8	7	anbi1i 625	. . . . . 6 ⊢ ((𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
9	8	exbii 1851	. . . . 5 ⊢ (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ ∃𝑦(∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
10	6, 9	mpbi 229	. . . 4 ⊢ ∃𝑦(∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣)
11		id 22	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
12		hbnae 2432	. . . . . . 7 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
13		hbn1 2139	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦)
14		ax-5 1914	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑣 → ∀𝑥 𝑧 = 𝑣)
15		ax-5 1914	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑣 → ∀𝑧 𝑦 = 𝑣)
16		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦)
17		equequ1 2029	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → (𝑧 = 𝑣 ↔ 𝑦 = 𝑣))
18	16, 17	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (𝑧 = 𝑣 ↔ 𝑦 = 𝑣))
19	18	idiALT 43238	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → (𝑧 = 𝑣 ↔ 𝑦 = 𝑣))
20	14, 15, 19	dvelimh 2450	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
21	11, 20	syl 17	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
22	21	idiALT 43238	. . . . . . . . . . . . 13 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
23	22	alimi 1814	. . . . . . . . . . . 12 ⊢ (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
24	13, 23	syl 17	. . . . . . . . . . 11 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
25	11, 24	syl 17	. . . . . . . . . 10 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
26		19.41rg 43311	. . . . . . . . . 10 ⊢ (∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣) → ((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
27	25, 26	syl 17	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
28	27	idiALT 43238	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
29	28	alimi 1814	. . . . . . 7 ⊢ (∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
30	12, 29	syl 17	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
31	11, 30	syl 17	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
32		exim 1837	. . . . 5 ⊢ (∀𝑦((∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → (∃𝑦(∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
33	31, 32	syl 17	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑦(∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
34		pm2.27 42	. . . 4 ⊢ (∃𝑦(∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((∃𝑦(∃𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)) → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))
35	10, 33, 34	mpsyl 68	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
36		excomim 2164	. . 3 ⊢ (∃𝑦∃𝑥(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
37	35, 36	syl 17	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
38	37	idiALT 43238	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1540  ∃wex 1782   ∈ wcel 2107  Vcvv 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-13 2372  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477

This theorem is referenced by:  ax6e2ndeq  43320  ax6e2ndeqVD  43670  ax6e2ndeqALT  43692