riota2df

Description: A deduction version of riota2f . (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	riota2df.1	$⊢ Ⅎ x φ$
	riota2df.2	$⊢ φ \to \underline{Ⅎ} x B$
	riota2df.3	$⊢ φ \to Ⅎ x χ$
	riota2df.4	$⊢ φ \to B \in A$
	riota2df.5	$⊢ (φ \land x = B) \to (ψ \leftrightarrow χ)$
Assertion	riota2df	$⊢ (φ \land \exists! x \in A ψ) \to (χ \leftrightarrow (ι x \in A \| ψ) = B)$

Proof

Step	Hyp	Ref	Expression
1		riota2df.1	$⊢ Ⅎ x φ$
2		riota2df.2	$⊢ φ \to \underline{Ⅎ} x B$
3		riota2df.3	$⊢ φ \to Ⅎ x χ$
4		riota2df.4	$⊢ φ \to B \in A$
5		riota2df.5	$⊢ (φ \land x = B) \to (ψ \leftrightarrow χ)$
6	4	adantr	$⊢ (φ \land \exists! x \in A ψ) \to B \in A$
7		df-reu	$⊢ \exists! x \in A ψ \leftrightarrow \exists! x (x \in A \land ψ)$
8	7	bilani	$⊢ (φ \land \exists! x \in A ψ) \to \exists! x (x \in A \land ψ)$
9		simpr	$⊢ ((φ \land \exists! x \in A ψ) \land x = B) \to x = B$
10	6	adantr	$⊢ ((φ \land \exists! x \in A ψ) \land x = B) \to B \in A$
11	9 10	eqeltrd	$⊢ ((φ \land \exists! x \in A ψ) \land x = B) \to x \in A$
12	11	biantrurd	$⊢ ((φ \land \exists! x \in A ψ) \land x = B) \to (ψ \leftrightarrow (x \in A \land ψ))$
13	5	adantlr	$⊢ ((φ \land \exists! x \in A ψ) \land x = B) \to (ψ \leftrightarrow χ)$
14	12 13	bitr3d	$⊢ ((φ \land \exists! x \in A ψ) \land x = B) \to ((x \in A \land ψ) \leftrightarrow χ)$
15		nfreu1	$⊢ Ⅎ x \exists! x \in A ψ$
16	1 15	nfan	$⊢ Ⅎ x (φ \land \exists! x \in A ψ)$
17	3	adantr	$⊢ (φ \land \exists! x \in A ψ) \to Ⅎ x χ$
18	2	adantr	$⊢ (φ \land \exists! x \in A ψ) \to \underline{Ⅎ} x B$
19	6 8 14 16 17 18	iota2df	$⊢ (φ \land \exists! x \in A ψ) \to (χ \leftrightarrow (ι x \| (x \in A \land ψ)) = B)$
20		df-riota	$⊢ (ι x \in A \| ψ) = (ι x \| (x \in A \land ψ))$
21	20	eqeq1i	$⊢ (ι x \in A \| ψ) = B \leftrightarrow (ι x \| (x \in A \land ψ)) = B$
22	19 21	bitr4di	$⊢ (φ \land \exists! x \in A ψ) \to (χ \leftrightarrow (ι x \in A \| ψ) = B)$

Metamath Proof Explorer

Theorem riota2df

Proof