2uasbanh

Description: Distribute the unabbreviated form of proper substitution in and out of a conjunction. 2uasbanh is derived from 2uasbanhVD . (Contributed by Alan Sare, 31-May-2014) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	2uasbanh.1	$⊢ χ \leftrightarrow (\exists x \exists y ((x = u \land y = v) \land φ) \land \exists x \exists y ((x = u \land y = v) \land ψ))$
	Assertion	2uasbanh	$⊢ \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		2uasbanh.1	$⊢ χ \leftrightarrow (\exists x \exists y ((x = u \land y = v) \land φ) \land \exists x \exists y ((x = u \land y = v) \land ψ))$
2		simpl	$⊢ ((x = u \land y = v) \land (φ \land ψ)) \to (x = u \land y = v)$
3		simprl	$⊢ ((x = u \land y = v) \land (φ \land ψ)) \to φ$
4	2 3	jca	$⊢ ((x = u \land y = v) \land (φ \land ψ)) \to ((x = u \land y = v) \land φ)$
5	4	2eximi	$⊢ \exists x \exists y ((x = u \land y = v) \land (φ \land ψ)) \to \exists x \exists y ((x = u \land y = v) \land φ)$
6		simprr	$⊢ ((x = u \land y = v) \land (φ \land ψ)) \to ψ$
7	2 6	jca	$⊢ ((x = u \land y = v) \land (φ \land ψ)) \to ((x = u \land y = v) \land ψ)$
8	7	2eximi	$⊢ \exists x \exists y ((x = u \land y = v) \land (φ \land ψ)) \to \exists x \exists y ((x = u \land y = v) \land ψ)$
9	5 8	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 ψ))$
10	1	simplbi	$⊢ χ \to \exists x \exists y ((x = u \land y = v) \land φ)$
11		simpl	$⊢ ((x = u \land y = v) \land φ) \to (x = u \land y = v)$
12	11	2eximi	$⊢ \exists x \exists y ((x = u \land y = v) \land φ) \to \exists x \exists y (x = u \land y = v)$
13	10 12	syl	$⊢ χ \to \exists x \exists y (x = u \land y = v)$
14		ax6e2ndeq	$⊢ (\neg \forall x x = y \lor u = v) \leftrightarrow \exists x \exists y (x = u \land y = v)$
15	13 14	sylibr	$⊢ χ \to (\neg \forall x x = y \lor u = v)$
16		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 φ))$
17	15 16	syl	$⊢ χ \to ([u/ x] [v/ y] φ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land φ))$
18	10 17	mpbird	$⊢ χ \to [u/ x] [v/ y] φ$
19	1	simprbi	$⊢ χ \to \exists x \exists y ((x = u \land y = v) \land ψ)$
20		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 ψ))$
21	15 20	syl	$⊢ χ \to ([u/ x] [v/ y] ψ \leftrightarrow \exists x \exists y ((x = u \land y = v) \land ψ))$
22	19 21	mpbird	$⊢ χ \to [u/ x] [v/ y] ψ$
23		sban	$⊢ [v/ y] (φ \land ψ) \leftrightarrow ([v/ y] φ \land [v/ y] ψ)$
24	23	sbbii	$⊢ [u/ x] [v/ y] (φ \land ψ) \leftrightarrow [u/ x] ([v/ y] φ \land [v/ y] ψ)$
25		sban	$⊢ [u/ x] ([v/ y] φ \land [v/ y] ψ) \leftrightarrow ([u/ x] [v/ y] φ \land [u/ x] [v/ y] ψ)$
26	24 25	bitri	$⊢ [u/ x] [v/ y] (φ \land ψ) \leftrightarrow ([u/ x] [v/ y] φ \land [u/ x] [v/ y] ψ)$
27	18 22 26	sylanbrc	$⊢ χ \to [u/ x] [v/ y] (φ \land ψ)$
28		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 ψ)))$
29	15 28	syl	$⊢ χ \to ([u/ x] [v/ y] (φ \land ψ) \leftrightarrow \exists x \exists y ((x = u \land y = v) \land (φ \land ψ)))$
30	27 29	mpbid	$⊢ χ \to \exists x \exists y ((x = u \land y = v) \land (φ \land ψ))$
31	1 30	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 ψ))$
32	9 31	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 ψ))$

Metamath Proof Explorer

Theorem 2uasbanh

Proof