rmoanim

Description: Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim . (Contributed by Alexander van der Vekens, 25-Jun-2017) Avoid ax-10 and ax-11 . (Revised by GG, 24-Aug-2023)

		Ref	Expression
	Hypothesis	rmoanim.1	$⊢ Ⅎ x φ$
	Assertion	rmoanim	$⊢ \exists^{} x \in A (φ \land ψ) \leftrightarrow (φ \to \exists^{} x \in A ψ)$

Proof

Step	Hyp	Ref	Expression
1		rmoanim.1	$⊢ Ⅎ x φ$
2		impexp	$⊢ ((φ \land ψ) \to x = y) \leftrightarrow (φ \to (ψ \to x = y))$
3	2	ralbii	$⊢ \forall x \in A ((φ \land ψ) \to x = y) \leftrightarrow \forall x \in A (φ \to (ψ \to x = y))$
4	1	r19.21	$⊢ \forall x \in A (φ \to (ψ \to x = y)) \leftrightarrow (φ \to \forall x \in A (ψ \to x = y))$
5	3 4	bitri	$⊢ \forall x \in A ((φ \land ψ) \to x = y) \leftrightarrow (φ \to \forall x \in A (ψ \to x = y))$
6	5	exbii	$⊢ \exists y \forall x \in A ((φ \land ψ) \to x = y) \leftrightarrow \exists y (φ \to \forall x \in A (ψ \to x = y))$
7		df-rmo	$⊢ \exists^{} x \in A (φ \land ψ) \leftrightarrow \exists^{} x (x \in A \land (φ \land ψ))$
8		dfmo	$⊢ \exists^{*} x (x \in A \land (φ \land ψ)) \leftrightarrow \exists y \forall x ((x \in A \land (φ \land ψ)) \to x = y)$
9		impexp	$⊢ ((x \in A \land (φ \land ψ)) \to x = y) \leftrightarrow (x \in A \to ((φ \land ψ) \to x = y))$
10	9	albii	$⊢ \forall x ((x \in A \land (φ \land ψ)) \to x = y) \leftrightarrow \forall x (x \in A \to ((φ \land ψ) \to x = y))$
11		df-ral	$⊢ \forall x \in A ((φ \land ψ) \to x = y) \leftrightarrow \forall x (x \in A \to ((φ \land ψ) \to x = y))$
12	10 11	bitr4i	$⊢ \forall x ((x \in A \land (φ \land ψ)) \to x = y) \leftrightarrow \forall x \in A ((φ \land ψ) \to x = y)$
13	12	exbii	$⊢ \exists y \forall x ((x \in A \land (φ \land ψ)) \to x = y) \leftrightarrow \exists y \forall x \in A ((φ \land ψ) \to x = y)$
14	7 8 13	3bitri	$⊢ \exists^{*} x \in A (φ \land ψ) \leftrightarrow \exists y \forall x \in A ((φ \land ψ) \to x = y)$
15		df-rmo	$⊢ \exists^{} x \in A ψ \leftrightarrow \exists^{} x (x \in A \land ψ)$
16		dfmo	$⊢ \exists^{*} x (x \in A \land ψ) \leftrightarrow \exists y \forall x ((x \in A \land ψ) \to x = y)$
17		impexp	$⊢ ((x \in A \land ψ) \to x = y) \leftrightarrow (x \in A \to (ψ \to x = y))$
18	17	albii	$⊢ \forall x ((x \in A \land ψ) \to x = y) \leftrightarrow \forall x (x \in A \to (ψ \to x = y))$
19		df-ral	$⊢ \forall x \in A (ψ \to x = y) \leftrightarrow \forall x (x \in A \to (ψ \to x = y))$
20	18 19	bitr4i	$⊢ \forall x ((x \in A \land ψ) \to x = y) \leftrightarrow \forall x \in A (ψ \to x = y)$
21	20	exbii	$⊢ \exists y \forall x ((x \in A \land ψ) \to x = y) \leftrightarrow \exists y \forall x \in A (ψ \to x = y)$
22	15 16 21	3bitri	$⊢ \exists^{*} x \in A ψ \leftrightarrow \exists y \forall x \in A (ψ \to x = y)$
23	22	imbi2i	$⊢ (φ \to \exists^{*} x \in A ψ) \leftrightarrow (φ \to \exists y \forall x \in A (ψ \to x = y))$
24		19.37v	$⊢ \exists y (φ \to \forall x \in A (ψ \to x = y)) \leftrightarrow (φ \to \exists y \forall x \in A (ψ \to x = y))$
25	23 24	bitr4i	$⊢ (φ \to \exists^{*} x \in A ψ) \leftrightarrow \exists y (φ \to \forall x \in A (ψ \to x = y))$
26	6 14 25	3bitr4i	$⊢ \exists^{} x \in A (φ \land ψ) \leftrightarrow (φ \to \exists^{} x \in A ψ)$

Metamath Proof Explorer

Theorem rmoanim

Proof