Theorem 2sb5ndALT 45504

Description: Equivalence for double substitution 2sb5 2312 without distinct 𝑥, 𝑦 requirement. 2sb5nd 45133 is derived from 2sb5ndVD 45482. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in 2sb5ndVD 45482. (Contributed by Alan Sare, 19-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
2sb5ndALT	⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))

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

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem 2sb5ndALT

Step	Hyp	Ref	Expression
1		ax6e2ndeq 45132	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
2		anabs5 673	. . . 4 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
3		2pm13.193 45125	. . . . . . . . 9 ⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
4	3	exbii 1868	. . . . . . . 8 ⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
5		hbs1 2308	. . . . . . . . . . . 12 ⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
6		id 22	. . . . . . . . . . . . 13 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)
7		axc11 2461	. . . . . . . . . . . . 13 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
8	6, 7	syl 17	. . . . . . . . . . . 12 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
9		pm3.33 774	. . . . . . . . . . . 12 ⊢ ((([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ∧ (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
10	5, 8, 9	sylancr 596	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
11		hbs1 2308	. . . . . . . . . . . . . 14 ⊢ ([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
12	11	sbt 2095	. . . . . . . . . . . . 13 ⊢ [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
13		sbi1 2103	. . . . . . . . . . . . 13 ⊢ ([𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑))
14	12, 13	ax-mp 5	. . . . . . . . . . . 12 ⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑)
15		id 22	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
16		axc11n 2457	. . . . . . . . . . . . . . 15 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑥 = 𝑦)
17	16	con3i 154	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑦 𝑦 = 𝑥)
18	15, 17	syl 17	. . . . . . . . . . . . 13 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑦 𝑦 = 𝑥)
19		sbal2 2560	. . . . . . . . . . . . 13 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
20	18, 19	syl 17	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
21		imbi2 350	. . . . . . . . . . . . 13 ⊢ (([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)))
22	21	biimpac 482	. . . . . . . . . . . 12 ⊢ ((([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑) ∧ ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
23	14, 20, 22	sylancr 596	. . . . . . . . . . 11 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
24	10, 23	pm2.61i 183	. . . . . . . . . 10 ⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
25	24	nf5i 2180	. . . . . . . . 9 ⊢ Ⅎ𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑
26	25	19.41 2270	. . . . . . . 8 ⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
27	4, 26	bitr3i 279	. . . . . . 7 ⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ↔ (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
28	27	exbii 1868	. . . . . 6 ⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ↔ ∃𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
29		nfs1v 2190	. . . . . . 7 ⊢ Ⅎ𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑
30	29	19.41 2270	. . . . . 6 ⊢ (∃𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
31	28, 30	bitr2i 278	. . . . 5 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
32	31	anbi2i 632	. . . 4 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))
33	2, 32	bitr3i 279	. . 3 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))
34		pm5.32 581	. . 3 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))) ↔ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))))
35	33, 34	mpbir 233	. 2 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))
36	1, 35	sylbi 219	1 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858  ∀wal 1558   = wceq 1560  ∃wex 1799  [wsb 2090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-13 2403  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3456

This theorem is referenced by: (None)