reuan

Description: Introduction of a conjunct into restricted unique existential quantifier, analogous to euan . (Contributed by Alexander van der Vekens, 2-Jul-2017)

		Ref	Expression
	Hypothesis	rmoanim.1	$⊢ Ⅎ x φ$
	Assertion	reuan	$⊢ \exists! x \in A (φ \land ψ) \leftrightarrow (φ \land \exists! x \in A ψ)$

Proof

Step	Hyp	Ref	Expression
1		rmoanim.1	$⊢ Ⅎ x φ$
2		simpl	$⊢ (φ \land ψ) \to φ$
3	2	a1i	$⊢ x \in A \to ((φ \land ψ) \to φ)$
4	1 3	rexlimi	$⊢ \exists x \in A (φ \land ψ) \to φ$
5	4	adantr	$⊢ (\exists x \in A (φ \land ψ) \land \exists^{*} x \in A (φ \land ψ)) \to φ$
6		simpr	$⊢ (φ \land ψ) \to ψ$
7	6	reximi	$⊢ \exists x \in A (φ \land ψ) \to \exists x \in A ψ$
8	7	adantr	$⊢ (\exists x \in A (φ \land ψ) \land \exists^{*} x \in A (φ \land ψ)) \to \exists x \in A ψ$
9		nfre1	$⊢ Ⅎ x \exists x \in A (φ \land ψ)$
10	4	adantr	$⊢ (\exists x \in A (φ \land ψ) \land x \in A) \to φ$
11	10	a1d	$⊢ (\exists x \in A (φ \land ψ) \land x \in A) \to (ψ \to φ)$
12	11	ancrd	$⊢ (\exists x \in A (φ \land ψ) \land x \in A) \to (ψ \to (φ \land ψ))$
13	6 12	impbid2	$⊢ (\exists x \in A (φ \land ψ) \land x \in A) \to ((φ \land ψ) \leftrightarrow ψ)$
14	9 13	rmobida	$⊢ \exists x \in A (φ \land ψ) \to (\exists^{} x \in A (φ \land ψ) \leftrightarrow \exists^{} x \in A ψ)$
15	14	biimpa	$⊢ (\exists x \in A (φ \land ψ) \land \exists^{} x \in A (φ \land ψ)) \to \exists^{} x \in A ψ$
16	5 8 15	jca32	$⊢ (\exists x \in A (φ \land ψ) \land \exists^{} x \in A (φ \land ψ)) \to (φ \land (\exists x \in A ψ \land \exists^{} x \in A ψ))$
17		reu5	$⊢ \exists! x \in A (φ \land ψ) \leftrightarrow (\exists x \in A (φ \land ψ) \land \exists^{*} x \in A (φ \land ψ))$
18		reu5	$⊢ \exists! x \in A ψ \leftrightarrow (\exists x \in A ψ \land \exists^{*} x \in A ψ)$
19	18	anbi2i	$⊢ (φ \land \exists! x \in A ψ) \leftrightarrow (φ \land (\exists x \in A ψ \land \exists^{*} x \in A ψ))$
20	16 17 19	3imtr4i	$⊢ \exists! x \in A (φ \land ψ) \to (φ \land \exists! x \in A ψ)$
21		ibar	$⊢ φ \to (ψ \leftrightarrow (φ \land ψ))$
22	21	adantr	$⊢ (φ \land x \in A) \to (ψ \leftrightarrow (φ \land ψ))$
23	1 22	reubida	$⊢ φ \to (\exists! x \in A ψ \leftrightarrow \exists! x \in A (φ \land ψ))$
24	23	biimpa	$⊢ (φ \land \exists! x \in A ψ) \to \exists! x \in A (φ \land ψ)$
25	20 24	impbii	$⊢ \exists! x \in A (φ \land ψ) \leftrightarrow (φ \land \exists! x \in A ψ)$

Metamath Proof Explorer

Theorem reuan

Proof