2sb5ndVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2sb5nd is 2sb5ndVD without virtual deductions and was automatically derived from 2sb5ndVD . (Contributed by Alan Sare, 30-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	2sb5ndVD	$⊢ (\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		idn1	$⊢ (\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	e1a	$⊢ (\forall x x = y \to (\forall x [u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ))$
9		imim1	$⊢ ([u/ x] [v/ y] φ \to \forall x [u/ x] [v/ y] φ) \to ((\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	e01	$⊢ (\forall x x = y \to ([u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ))$
11	10	in1	$⊢ \forall x x = y \to ([u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ)$
12		hbs1	$⊢ [v/ y] φ \to \forall y [v/ y] φ$
13	12	sbt	$⊢ [u/ x] ([v/ y] φ \to \forall y [v/ y] φ)$
14		sbi1	$⊢ [u/ x] ([v/ y] φ \to \forall y [v/ y] φ) \to ([u/ x] [v/ y] φ \to [u/ x] \forall y [v/ y] φ)$
15	13 14	e0a	$⊢ [u/ x] [v/ y] φ \to [u/ x] \forall y [v/ y] φ$
16		idn1	$⊢ (\neg \forall x x = y \to \neg \forall x x = y)$
17		axc11n	$⊢ \forall y y = x \to \forall x x = y$
18	17	con3i	$⊢ \neg \forall x x = y \to \neg \forall y y = x$
19	16 18	e1a	$⊢ (\neg \forall x x = y \to \neg \forall y y = x)$
20		sbal2	$⊢ \neg \forall y y = x \to ([u/ x] \forall y [v/ y] φ \leftrightarrow \forall y [u/ x] [v/ y] φ)$
21	19 20	e1a	$⊢ (\neg \forall x x = y \to ([u/ x] \forall y [v/ y] φ \leftrightarrow \forall y [u/ x] [v/ y] φ))$
22		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] φ))$
23	22	biimpcd	$⊢ ([u/ x] [v/ y] φ \to [u/ x] \forall y [v/ y] φ) \to (([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] φ))$
24	15 21 23	e01	$⊢ (\neg \forall x x = y \to ([u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ))$
25	24	in1	$⊢ \neg \forall x x = y \to ([u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ)$
26	11 25	pm2.61i	$⊢ [u/ x] [v/ y] φ \to \forall y [u/ x] [v/ y] φ$
27	26	nf5i	$⊢ Ⅎ y [u/ x] [v/ y] φ$
28	27	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] φ)$
29	4 28	bitr3i	$⊢ \exists y ((x = u \land y = v) \land φ) \leftrightarrow (\exists y (x = u \land y = v) \land [u/ x] [v/ y] φ)$
30	29	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] φ)$
31	5	nf5i	$⊢ Ⅎ x [u/ x] [v/ y] φ$
32	31	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] φ)$
33	30 32	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 φ)$
34	33	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 φ))$
35	2 34	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 φ))$
36		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 φ)))$
37	35 36	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 φ))$
38	1 37	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 φ))$

1::	\|- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )
2:1:	\|- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. y ( ( x = u /\ y = v ) /\ ph ) )
3::	\|- ( [ v / y ] ph -> A. y [ v / y ] ph )
4:3:	\|- [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph )
5:4:	\|- ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph )
6::	\|- (. -. A. x x = y ->. -. A. x x = y ).
7::	\|- ( A. y y = x -> A. x x = y )
8:7:	\|- ( -. A. x x = y -> -. A. y y = x )
9:6,8:	\|- (. -. A. x x = y ->. -. A. y y = x ).
10:9:	\|- ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph )
11:5,10:	\|- ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
12:11:	\|- ( -. A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
13::	\|- ( [ u / x ] [ v / y ] ph -> A. x [ u / x ] [ v / y ] ph )
14::	\|- (. A. x x = y ->. A. x x = y ).
15:14:	\|- (. A. x x = y ->. ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
16:13,15:	\|- (. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
17:16:	\|- ( A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
19:12,17:	\|- ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
20:19:	\|- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
21:2,20:	\|- ( E. y ( ( x = u /\ y = v ) /\ ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
22:21:	\|- ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) <-> E. x ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
23:13:	\|- ( E. x ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
24:22,23:	\|- ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
240:24:	\|- ( ( E. x E. y ( x = u /\ y = v ) /\ ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
241::	\|- ( ( E. x E. y ( x = u /\ y = v ) /\ ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ) <-> ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
242:241,240:	\|- ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
243::	\|- ( ( E. x E. y ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ) <-> ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ) )
25:242,243:	\|- ( E. x E. y ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
26::	\|- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )
qed:25,26:	\|- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )

Metamath Proof Explorer

Theorem 2sb5ndVD

Proof