rmo4

Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006) (Revised by NM, 16-Jun-2017)

		Ref	Expression
	Hypothesis	rmo4.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	Assertion	rmo4	$⊢ \exists^{*} x \in A φ \leftrightarrow \forall x \in A \forall y \in A ((φ \land ψ) \to x = y)$

Proof

Step	Hyp	Ref	Expression
1		rmo4.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		df-rmo	$⊢ \exists^{} x \in A φ \leftrightarrow \exists^{} x (x \in A \land φ)$
3		an4	$⊢ ((x \in A \land φ) \land (y \in A \land ψ)) \leftrightarrow ((x \in A \land y \in A) \land (φ \land ψ))$
4		ancom	$⊢ (x \in A \land y \in A) \leftrightarrow (y \in A \land x \in A)$
5	4	anbi1i	$⊢ ((x \in A \land y \in A) \land (φ \land ψ)) \leftrightarrow ((y \in A \land x \in A) \land (φ \land ψ))$
6	3 5	bitri	$⊢ ((x \in A \land φ) \land (y \in A \land ψ)) \leftrightarrow ((y \in A \land x \in A) \land (φ \land ψ))$
7	6	imbi1i	$⊢ (((x \in A \land φ) \land (y \in A \land ψ)) \to x = y) \leftrightarrow (((y \in A \land x \in A) \land (φ \land ψ)) \to x = y)$
8		impexp	$⊢ (((y \in A \land x \in A) \land (φ \land ψ)) \to x = y) \leftrightarrow ((y \in A \land x \in A) \to ((φ \land ψ) \to x = y))$
9		impexp	$⊢ ((y \in A \land x \in A) \to ((φ \land ψ) \to x = y)) \leftrightarrow (y \in A \to (x \in A \to ((φ \land ψ) \to x = y)))$
10	7 8 9	3bitri	$⊢ (((x \in A \land φ) \land (y \in A \land ψ)) \to x = y) \leftrightarrow (y \in A \to (x \in A \to ((φ \land ψ) \to x = y)))$
11	10	albii	$⊢ \forall y (((x \in A \land φ) \land (y \in A \land ψ)) \to x = y) \leftrightarrow \forall y (y \in A \to (x \in A \to ((φ \land ψ) \to x = y)))$
12		df-ral	$⊢ \forall y \in A (x \in A \to ((φ \land ψ) \to x = y)) \leftrightarrow \forall y (y \in A \to (x \in A \to ((φ \land ψ) \to x = y)))$
13		r19.21v	$⊢ \forall y \in A (x \in A \to ((φ \land ψ) \to x = y)) \leftrightarrow (x \in A \to \forall y \in A ((φ \land ψ) \to x = y))$
14	11 12 13	3bitr2i	$⊢ \forall y (((x \in A \land φ) \land (y \in A \land ψ)) \to x = y) \leftrightarrow (x \in A \to \forall y \in A ((φ \land ψ) \to x = y))$
15	14	albii	$⊢ \forall x \forall y (((x \in A \land φ) \land (y \in A \land ψ)) \to x = y) \leftrightarrow \forall x (x \in A \to \forall y \in A ((φ \land ψ) \to x = y))$
16		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
17	16 1	anbi12d	$⊢ x = y \to ((x \in A \land φ) \leftrightarrow (y \in A \land ψ))$
18	17	mo4	$⊢ \exists^{*} x (x \in A \land φ) \leftrightarrow \forall x \forall y (((x \in A \land φ) \land (y \in A \land ψ)) \to x = y)$
19		df-ral	$⊢ \forall x \in A \forall y \in A ((φ \land ψ) \to x = y) \leftrightarrow \forall x (x \in A \to \forall y \in A ((φ \land ψ) \to x = y))$
20	15 18 19	3bitr4i	$⊢ \exists^{*} x (x \in A \land φ) \leftrightarrow \forall x \in A \forall y \in A ((φ \land ψ) \to x = y)$
21	2 20	bitri	$⊢ \exists^{*} x \in A φ \leftrightarrow \forall x \in A \forall y \in A ((φ \land ψ) \to x = y)$

Metamath Proof Explorer

Theorem rmo4

Proof