2uasbanhVD

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. 2uasbanh is 2uasbanhVD without virtual deductions and was automatically derived from 2uasbanhVD . (Contributed by Alan Sare, 31-May-2014) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	2uasbanhVD.1	$⊢ χ \leftrightarrow (\exists x \exists y ((x = u \land y = v) \land φ) \land \exists x \exists y ((x = u \land y = v) \land ψ))$
	Assertion	2uasbanhVD	$⊢ \exists x \exists y ((x = u \land y = v) \land (φ \land ψ)) \leftrightarrow (\exists x \exists y ((x = u \land y = v) \land φ) \land \exists x \exists y ((x = u \land y = v) \land ψ))$

Proof

Step	Hyp	Ref	Expression
1		2uasbanhVD.1	$⊢ χ \leftrightarrow (\exists x \exists y ((x = u \land y = v) \land φ) \land \exists x \exists y ((x = u \land y = v) \land ψ))$
2		idn1	$⊢ (((x = u \land y = v) \land (φ \land ψ)) \to ((x = u \land y = v) \land (φ \land ψ)))$
3		simpl	$⊢ ((x = u \land y = v) \land (φ \land ψ)) \to (x = u \land y = v)$
4	2 3	e1a	$⊢ (((x = u \land y = v) \land (φ \land ψ)) \to (x = u \land y = v))$
5		simpr	$⊢ ((x = u \land y = v) \land (φ \land ψ)) \to (φ \land ψ)$
6	2 5	e1a	$⊢ (((x = u \land y = v) \land (φ \land ψ)) \to (φ \land ψ))$
7		simpl	$⊢ (φ \land ψ) \to φ$
8	6 7	e1a	$⊢ (((x = u \land y = v) \land (φ \land ψ)) \to φ)$
9		pm3.2	$⊢ (x = u \land y = v) \to (φ \to ((x = u \land y = v) \land φ))$
10	4 8 9	e11	$⊢ (((x = u \land y = v) \land (φ \land ψ)) \to ((x = u \land y = v) \land φ))$
11	10	in1	$⊢ ((x = u \land y = v) \land (φ \land ψ)) \to ((x = u \land y = v) \land φ)$
12	11	eximi	$⊢ \exists y ((x = u \land y = v) \land (φ \land ψ)) \to \exists y ((x = u \land y = v) \land φ)$
13	12	eximi	$⊢ \exists x \exists y ((x = u \land y = v) \land (φ \land ψ)) \to \exists x \exists y ((x = u \land y = v) \land φ)$
14		simpr	$⊢ (φ \land ψ) \to ψ$
15	6 14	e1a	$⊢ (((x = u \land y = v) \land (φ \land ψ)) \to ψ)$
16		pm3.2	$⊢ (x = u \land y = v) \to (ψ \to ((x = u \land y = v) \land ψ))$
17	4 15 16	e11	$⊢ (((x = u \land y = v) \land (φ \land ψ)) \to ((x = u \land y = v) \land ψ))$
18	17	in1	$⊢ ((x = u \land y = v) \land (φ \land ψ)) \to ((x = u \land y = v) \land ψ)$
19	18	eximi	$⊢ \exists y ((x = u \land y = v) \land (φ \land ψ)) \to \exists y ((x = u \land y = v) \land ψ)$
20	19	eximi	$⊢ \exists x \exists y ((x = u \land y = v) \land (φ \land ψ)) \to \exists x \exists y ((x = u \land y = v) \land ψ)$
21	13 20	jca	$⊢ \exists x \exists y ((x = u \land y = v) \land (φ \land ψ)) \to (\exists x \exists y ((x = u \land y = v) \land φ) \land \exists x \exists y ((x = u \land y = v) \land ψ))$
22	1	biimpi	$⊢ χ \to (\exists x \exists y ((x = u \land y = v) \land φ) \land \exists x \exists y ((x = u \land y = v) \land ψ))$
23	22	dfvd1ir	$⊢ (χ \to (\exists x \exists y ((x = u \land y = v) \land φ) \land \exists x \exists y ((x = u \land y = v) \land ψ)))$
24		simpl	$⊢ (\exists x \exists y ((x = u \land y = v) \land φ) \land \exists x \exists y ((x = u \land y = v) \land ψ)) \to \exists x \exists y ((x = u \land y = v) \land φ)$
25	23 24	e1a	$⊢ (χ \to \exists x \exists y ((x = u \land y = v) \land φ))$
26		simpl	$⊢ ((x = u \land y = v) \land φ) \to (x = u \land y = v)$
27	26	2eximi	$⊢ \exists x \exists y ((x = u \land y = v) \land φ) \to \exists x \exists y (x = u \land y = v)$
28	25 27	e1a	$⊢ (χ \to \exists x \exists y (x = u \land y = v))$
29		ax6e2ndeq	$⊢ (\neg \forall x x = y \lor u = v) \leftrightarrow \exists x \exists y (x = u \land y = v)$
30	29	biimpri	$⊢ \exists x \exists y (x = u \land y = v) \to (\neg \forall x x = y \lor u = v)$
31	28 30	e1a	$⊢ (χ \to (\neg \forall x x = y \lor u = v))$
32		2sb5nd	$⊢ (\neg \forall x x = y \lor u = v) \to ([u/ x] [v/ y] φ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land φ))$
33	31 32	e1a	$⊢ (χ \to ([u/ x] [v/ y] φ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land φ)))$
34		biimpr	$⊢ ([u/ x] [v/ y] φ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land φ)) \to (\exists x \exists y ((x = u \land y = v) \land φ) \to [u/ x] [v/ y] φ)$
35	34	com12	$⊢ \exists x \exists y ((x = u \land y = v) \land φ) \to (([u/ x] [v/ y] φ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land φ)) \to [u/ x] [v/ y] φ)$
36	25 33 35	e11	$⊢ (χ \to [u/ x] [v/ y] φ)$
37		simpr	$⊢ (\exists x \exists y ((x = u \land y = v) \land φ) \land \exists x \exists y ((x = u \land y = v) \land ψ)) \to \exists x \exists y ((x = u \land y = v) \land ψ)$
38	23 37	e1a	$⊢ (χ \to \exists x \exists y ((x = u \land y = v) \land ψ))$
39		2sb5nd	$⊢ (\neg \forall x x = y \lor u = v) \to ([u/ x] [v/ y] ψ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land ψ))$
40	31 39	e1a	$⊢ (χ \to ([u/ x] [v/ y] ψ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land ψ)))$
41		biimpr	$⊢ ([u/ x] [v/ y] ψ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land ψ)) \to (\exists x \exists y ((x = u \land y = v) \land ψ) \to [u/ x] [v/ y] ψ)$
42	41	com12	$⊢ \exists x \exists y ((x = u \land y = v) \land ψ) \to (([u/ x] [v/ y] ψ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land ψ)) \to [u/ x] [v/ y] ψ)$
43	38 40 42	e11	$⊢ (χ \to [u/ x] [v/ y] ψ)$
44		sban	$⊢ [v/ y] (φ \land ψ) \leftrightarrow ([v/ y] φ \land [v/ y] ψ)$
45	44	sbbii	$⊢ [u/ x] [v/ y] (φ \land ψ) \leftrightarrow [u/ x] ([v/ y] φ \land [v/ y] ψ)$
46		sban	$⊢ [u/ x] ([v/ y] φ \land [v/ y] ψ) \leftrightarrow ([u/ x] [v/ y] φ \land [u/ x] [v/ y] ψ)$
47	45 46	bitri	$⊢ [u/ x] [v/ y] (φ \land ψ) \leftrightarrow ([u/ x] [v/ y] φ \land [u/ x] [v/ y] ψ)$
48		simplbi2comt	$⊢ ([u/ x] [v/ y] (φ \land ψ) \leftrightarrow ([u/ x] [v/ y] φ \land [u/ x] [v/ y] ψ)) \to ([u/ x] [v/ y] ψ \to ([u/ x] [v/ y] φ \to [u/ x] [v/ y] (φ \land ψ)))$
49	48	com13	$⊢ [u/ x] [v/ y] φ \to ([u/ x] [v/ y] ψ \to (([u/ x] [v/ y] (φ \land ψ) \leftrightarrow ([u/ x] [v/ y] φ \land [u/ x] [v/ y] ψ)) \to [u/ x] [v/ y] (φ \land ψ)))$
50	36 43 47 49	e110	$⊢ (χ \to [u/ x] [v/ y] (φ \land ψ))$
51		2sb5nd	$⊢ (\neg \forall x x = y \lor u = v) \to ([u/ x] [v/ y] (φ \land ψ) \leftrightarrow \exists x \exists y ((x = u \land y = v) \land (φ \land ψ)))$
52	31 51	e1a	$⊢ (χ \to ([u/ x] [v/ y] (φ \land ψ) \leftrightarrow \exists x \exists y ((x = u \land y = v) \land (φ \land ψ))))$
53		biimp	$⊢ ([u/ x] [v/ y] (φ \land ψ) \leftrightarrow \exists x \exists y ((x = u \land y = v) \land (φ \land ψ))) \to ([u/ x] [v/ y] (φ \land ψ) \to \exists x \exists y ((x = u \land y = v) \land (φ \land ψ)))$
54	53	com12	$⊢ [u/ x] [v/ y] (φ \land ψ) \to (([u/ x] [v/ y] (φ \land ψ) \leftrightarrow \exists x \exists y ((x = u \land y = v) \land (φ \land ψ))) \to \exists x \exists y ((x = u \land y = v) \land (φ \land ψ)))$
55	50 52 54	e11	$⊢ (χ \to \exists x \exists y ((x = u \land y = v) \land (φ \land ψ)))$
56	55	in1	$⊢ χ \to \exists x \exists y ((x = u \land y = v) \land (φ \land ψ))$
57	1 56	sylbir	$⊢ (\exists x \exists y ((x = u \land y = v) \land φ) \land \exists x \exists y ((x = u \land y = v) \land ψ)) \to \exists x \exists y ((x = u \land y = v) \land (φ \land ψ))$
58	21 57	impbii	$⊢ \exists x \exists y ((x = u \land y = v) \land (φ \land ψ)) \leftrightarrow (\exists x \exists y ((x = u \land y = v) \land φ) \land \exists x \exists y ((x = u \land y = v) \land ψ))$

h1::	\|- ( ch <-> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
100:1:	\|- ( ch -> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
2:100:	\|- (. ch ->. ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) ).
3:2:	\|- (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ph ) ).
4:3:	\|- (. ch ->. E. x E. y ( x = u /\ y = v ) ).
5:4:	\|- (. ch ->. ( -. A. x x = y \/ u = v ) ).
6:5:	\|- (. ch ->. ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ).
7:3,6:	\|- (. ch ->. [ u / x ] [ v / y ] ph ).
8:2:	\|- (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ps ) ).
9:5:	\|- (. ch ->. ( [ u / x ] [ v / y ] ps <-> E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) ).
10:8,9:	\|- (. ch ->. [ u / x ] [ v / y ] ps ).
101::	\|- ( [ v / y ] ( ph /\ ps ) <-> ( [ v / y ] ph /\ [ v / y ] ps ) )
102:101:	\|- ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> [ u / x ] ( [ v / y ] ph /\ [ v / y ] ps ) )
103::	\|- ( [ u / x ] ( [ v / y ] ph /\ [ v / y ] ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) )
104:102,103:	\|- ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) )
11:7,10,104:	\|- (. ch ->. [ u / x ] [ v / y ] ( ph /\ ps ) ).
110:5:	\|- (. ch ->. ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ) ).
12:11,110:	\|- (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ).
120:12:	\|- ( ch -> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) )
13:1,120:	\|- ( ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) )
14::	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ).
15:14:	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( x = u /\ y = v ) ).
16:14:	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ph /\ ps ) ).
17:16:	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ph ).
18:15,17:	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ph ) ).
19:18:	\|- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ( x = u /\ y = v ) /\ ph ) )
20:19:	\|- ( E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. y ( ( x = u /\ y = v ) /\ ph ) )
21:20:	\|- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
22:16:	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ps ).
23:15,22:	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ps ) ).
24:23:	\|- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ( x = u /\ y = v ) /\ ps ) )
25:24:	\|- ( E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. y ( ( x = u /\ y = v ) /\ ps ) )
26:25:	\|- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ps ) )
27:21,26:	\|- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
qed:13,27:	\|- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) <-> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )

Metamath Proof Explorer

Theorem 2uasbanhVD

Proof