2sb5ndALT

Description: Equivalence for double substitution 2sb5 without distinct x , y requirement. 2sb5nd is derived from 2sb5ndVD . 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 . (Contributed by Alan Sare, 19-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	2sb5ndALT	$⊢ (\neg \forall x x = y \lor u = v) \to ([u/ x] [v/ y] φ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land φ))$

Proof

Step	Hyp	Ref	Expression
1		ax6e2ndeq	$⊢ (\neg \forall x x = y \lor u = v) \leftrightarrow \exists x \exists y (x = u \land y = v)$
2		anabs5	$⊢ (\exists x \exists y (x = u \land y = v) \land (\exists x \exists y (x = u \land y = v) \land [u/ x] [v/ y] φ)) \leftrightarrow (\exists x \exists y (x = u \land y = v) \land [u/ x] [v/ y] φ)$
3		2pm13.193	$⊢ ((x = u \land y = v) \land [u/ x] [v/ y] φ) \leftrightarrow ((x = u \land y = v) \land φ)$
4	3	exbii	$⊢ \exists y ((x = u \land y = v) \land [u/ x] [v/ y] φ) \leftrightarrow \exists y ((x = u \land y = v) \land φ)$
5		hbs1	$⊢ [u/ x] [v/ y] φ \to \forall x [u/ x] [v/ y] φ$
6		id	$⊢ \forall x x = y \to \forall x x = y$
7		axc11	$⊢ \forall x x = y \to (\forall x [u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ)$
8	6 7	syl	$⊢ \forall x x = y \to (\forall x [u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ)$
9		pm3.33	$⊢ (([u/ x] [v/ y] φ \to \forall x [u/ x] [v/ y] φ) \land (\forall x [u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ)) \to ([u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ)$
10	5 8 9	sylancr	$⊢ \forall x x = y \to ([u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ)$
11		hbs1	$⊢ [v/ y] φ \to \forall y [v/ y] φ$
12	11	sbt	$⊢ [u/ x] ([v/ y] φ \to \forall y [v/ y] φ)$
13		sbi1	$⊢ [u/ x] ([v/ y] φ \to \forall y [v/ y] φ) \to ([u/ x] [v/ y] φ \to [u/ x] \forall y [v/ y] φ)$
14	12 13	ax-mp	$⊢ [u/ x] [v/ y] φ \to [u/ x] \forall y [v/ y] φ$
15		id	$⊢ \neg \forall x x = y \to \neg \forall x x = y$
16		axc11n	$⊢ \forall y y = x \to \forall x x = y$
17	16	con3i	$⊢ \neg \forall x x = y \to \neg \forall y y = x$
18	15 17	syl	$⊢ \neg \forall x x = y \to \neg \forall y y = x$
19		sbal2	$⊢ \neg \forall y y = x \to ([u/ x] \forall y [v/ y] φ \leftrightarrow \forall y [u/ x] [v/ y] φ)$
20	18 19	syl	$⊢ \neg \forall x x = y \to ([u/ x] \forall y [v/ y] φ \leftrightarrow \forall y [u/ x] [v/ y] φ)$
21		imbi2	$⊢ ([u/ x] \forall y [v/ y] φ \leftrightarrow \forall y [u/ x] [v/ y] φ) \to (([u/ x] [v/ y] φ \to [u/ x] \forall y [v/ y] φ) \leftrightarrow ([u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ))$
22	21	biimpac	$⊢ (([u/ x] [v/ y] φ \to [u/ x] \forall y [v/ y] φ) \land ([u/ x] \forall y [v/ y] φ \leftrightarrow \forall y [u/ x] [v/ y] φ)) \to ([u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ)$
23	14 20 22	sylancr	$⊢ \neg \forall x x = y \to ([u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ)$
24	10 23	pm2.61i	$⊢ [u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ$
25	24	nf5i	$⊢ Ⅎ y [u/ x] [v/ y] φ$
26	25	19.41	$⊢ \exists y ((x = u \land y = v) \land [u/ x] [v/ y] φ) \leftrightarrow (\exists y (x = u \land y = v) \land [u/ x] [v/ y] φ)$
27	4 26	bitr3i	$⊢ \exists y ((x = u \land y = v) \land φ) \leftrightarrow (\exists y (x = u \land y = v) \land [u/ x] [v/ y] φ)$
28	27	exbii	$⊢ \exists x \exists y ((x = u \land y = v) \land φ) \leftrightarrow \exists x (\exists y (x = u \land y = v) \land [u/ x] [v/ y] φ)$
29		nfs1v	$⊢ Ⅎ x [u/ x] [v/ y] φ$
30	29	19.41	$⊢ \exists x (\exists y (x = u \land y = v) \land [u/ x] [v/ y] φ) \leftrightarrow (\exists x \exists y (x = u \land y = v) \land [u/ x] [v/ y] φ)$
31	28 30	bitr2i	$⊢ (\exists x \exists y (x = u \land y = v) \land [u/ x] [v/ y] φ) \leftrightarrow \exists x \exists y ((x = u \land y = v) \land φ)$
32	31	anbi2i	$⊢ (\exists x \exists y (x = u \land y = v) \land (\exists x \exists y (x = u \land y = v) \land [u/ x] [v/ y] φ)) \leftrightarrow (\exists x \exists y (x = u \land y = v) \land \exists x \exists y ((x = u \land y = v) \land φ))$
33	2 32	bitr3i	$⊢ (\exists x \exists y (x = u \land y = v) \land [u/ x] [v/ y] φ) \leftrightarrow (\exists x \exists y (x = u \land y = v) \land \exists x \exists y ((x = u \land y = v) \land φ))$
34		pm5.32	$⊢ (\exists x \exists y (x = u \land y = v) \to ([u/ x] [v/ y] φ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land φ))) \leftrightarrow ((\exists x \exists y (x = u \land y = v) \land [u/ x] [v/ y] φ) \leftrightarrow (\exists x \exists y (x = u \land y = v) \land \exists x \exists y ((x = u \land y = v) \land φ)))$
35	33 34	mpbir	$⊢ \exists x \exists y (x = u \land y = v) \to ([u/ x] [v/ y] φ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land φ))$
36	1 35	sylbi	$⊢ (\neg \forall x x = y \lor u = v) \to ([u/ x] [v/ y] φ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land φ))$

Metamath Proof Explorer

Theorem 2sb5ndALT

Proof