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	3 4	bianbi	$⊢ ((x \in A \land φ) \land (y \in A \land ψ)) \leftrightarrow ((y \in A \land x \in A) \land (φ \land ψ))$
6	5	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)$
7		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))$
8		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)))$
9	6 7 8	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)))$
10	9	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)))$
11		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)))$
12		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))$
13	10 11 12	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))$
14	13	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))$
15		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
16	15 1	anbi12d	$⊢ x = y \to ((x \in A \land φ) \leftrightarrow (y \in A \land ψ))$
17	16	mo4	$⊢ \exists^{*} x (x \in A \land φ) \leftrightarrow \forall x \forall y (((x \in A \land φ) \land (y \in A \land ψ)) \to x = y)$
18		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))$
19	14 17 18	3bitr4i	$⊢ \exists^{*} x (x \in A \land φ) \leftrightarrow \forall x \in A \forall y \in A ((φ \land ψ) \to x = y)$
20	2 19	bitri	$⊢ \exists^{*} x \in A φ \leftrightarrow \forall x \in A \forall y \in A ((φ \land ψ) \to x = y)$

Metamath Proof Explorer

Theorem rmo4

Proof