Theorem 2sb5ndALT 45640

Description: Equivalence for double substitution 2sb5 2313 without distinct 𝑥, 𝑦 requirement. 2sb5nd 45269 is derived from 2sb5ndVD 45618. 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 45618. (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 45268	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
2		anabs5 675	. . . 4 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
3		2pm13.193 45261	. . . . . . . . 9 ⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
4	3	exbii 1878	. . . . . . . 8 ⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
5		hbs1 2309	. . . . . . . . . . . 12 ⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
6		id 23	. . . . . . . . . . . . 13 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)
7		axc11 2462	. . . . . . . . . . . . 13 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
8	6, 7	syl 18	. . . . . . . . . . . 12 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
9		pm3.33 776	. . . . . . . . . . . 12 ⊢ ((([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ∧ (∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
10	5, 8, 9	sylancr 598	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
11		hbs1 2309	. . . . . . . . . . . . . 14 ⊢ ([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
12	11	sbt 2100	. . . . . . . . . . . . 13 ⊢ [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
13		sbi1 2105	. . . . . . . . . . . . 13 ⊢ ([𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑))
14	12, 13	ax-mp 5	. . . . . . . . . . . 12 ⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑)
15		id 23	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
16		axc11n 2458	. . . . . . . . . . . . . . 15 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑥 = 𝑦)
17	16	con3i 155	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑦 𝑦 = 𝑥)
18	15, 17	syl 18	. . . . . . . . . . . . 13 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑦 𝑦 = 𝑥)
19		sbal2 2561	. . . . . . . . . . . . 13 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
20	18, 19	syl 18	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
21		imbi2 351	. . . . . . . . . . . . 13 ⊢ (([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)))
22	21	biimpac 483	. . . . . . . . . . . 12 ⊢ ((([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑) ∧ ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
23	14, 20, 22	sylancr 598	. . . . . . . . . . 11 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
24	10, 23	pm2.61i 184	. . . . . . . . . 10 ⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
25	24	nf5i 2181	. . . . . . . . 9 ⊢ Ⅎ𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑
26	25	19.41 2271	. . . . . . . 8 ⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
27	4, 26	bitr3i 280	. . . . . . 7 ⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ↔ (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
28	27	exbii 1878	. . . . . 6 ⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ↔ ∃𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
29		nfs1v 2191	. . . . . . 7 ⊢ Ⅎ𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑
30	29	19.41 2271	. . . . . 6 ⊢ (∃𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
31	28, 30	bitr2i 279	. . . . 5 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
32	31	anbi2i 634	. . . 4 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))
33	2, 32	bitr3i 280	. . 3 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))
34		pm5.32 583	. . 3 ⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))) ↔ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))))
35	33, 34	mpbir 234	. 2 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))
36	1, 35	sylbi 220	1 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860  ∀wal 1568   = wceq 1570  ∃wex 1809  [wsb 2096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-13 2404  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3457

This theorem is referenced by: (None)