riotasv2d

Description: Value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 ). Special case of riota2f . (Contributed by NM, 2-Mar-2013)

	Ref	Expression
Hypotheses	riotasv2d.1	$⊢ Ⅎ y φ$
	riotasv2d.2	$⊢ φ \to \underline{Ⅎ} y F$
	riotasv2d.3	$⊢ φ \to Ⅎ y χ$
	riotasv2d.4	$⊢ φ \to D = (ι x \in A \| \forall y \in B (ψ \to x = C))$
	riotasv2d.5	$⊢ (φ \land y = E) \to (ψ \leftrightarrow χ)$
	riotasv2d.6	$⊢ (φ \land y = E) \to C = F$
	riotasv2d.7	$⊢ φ \to D \in A$
	riotasv2d.8	$⊢ φ \to E \in B$
	riotasv2d.9	$⊢ φ \to χ$
Assertion	riotasv2d	$⊢ (φ \land A \in V) \to D = F$

Proof

Step	Hyp	Ref	Expression
1		riotasv2d.1	$⊢ Ⅎ y φ$
2		riotasv2d.2	$⊢ φ \to \underline{Ⅎ} y F$
3		riotasv2d.3	$⊢ φ \to Ⅎ y χ$
4		riotasv2d.4	$⊢ φ \to D = (ι x \in A \| \forall y \in B (ψ \to x = C))$
5		riotasv2d.5	$⊢ (φ \land y = E) \to (ψ \leftrightarrow χ)$
6		riotasv2d.6	$⊢ (φ \land y = E) \to C = F$
7		riotasv2d.7	$⊢ φ \to D \in A$
8		riotasv2d.8	$⊢ φ \to E \in B$
9		riotasv2d.9	$⊢ φ \to χ$
10		elex	$⊢ A \in V \to A \in V$
11	8	adantr	$⊢ (φ \land A \in V) \to E \in B$
12	9	adantr	$⊢ (φ \land A \in V) \to χ$
13		eleq1	$⊢ y = E \to (y \in B \leftrightarrow E \in B)$
14	13	adantl	$⊢ (φ \land y = E) \to (y \in B \leftrightarrow E \in B)$
15	14 5	anbi12d	$⊢ (φ \land y = E) \to ((y \in B \land ψ) \leftrightarrow (E \in B \land χ))$
16	6	eqeq2d	$⊢ (φ \land y = E) \to (D = C \leftrightarrow D = F)$
17	15 16	imbi12d	$⊢ (φ \land y = E) \to (((y \in B \land ψ) \to D = C) \leftrightarrow ((E \in B \land χ) \to D = F))$
18	17	adantlr	$⊢ ((φ \land A \in V) \land y = E) \to (((y \in B \land ψ) \to D = C) \leftrightarrow ((E \in B \land χ) \to D = F))$
19	4 7	riotasvd	$⊢ (φ \land A \in V) \to ((y \in B \land ψ) \to D = C)$
20		nfv	$⊢ Ⅎ y A \in V$
21	1 20	nfan	$⊢ Ⅎ y (φ \land A \in V)$
22		nfcvd	$⊢ (φ \land A \in V) \to \underline{Ⅎ} y E$
23		nfvd	$⊢ φ \to Ⅎ y E \in B$
24	23 3	nfand	$⊢ φ \to Ⅎ y (E \in B \land χ)$
25		nfra1	$⊢ Ⅎ y \forall y \in B (ψ \to x = C)$
26		nfcv	$⊢ \underline{Ⅎ} y A$
27	25 26	nfriota	$⊢ \underline{Ⅎ} y (ι x \in A \| \forall y \in B (ψ \to x = C))$
28	1 4	nfceqdf	$⊢ φ \to (\underline{Ⅎ} y D \leftrightarrow \underline{Ⅎ} y (ι x \in A \| \forall y \in B (ψ \to x = C)))$
29	27 28	mpbiri	$⊢ φ \to \underline{Ⅎ} y D$
30	29 2	nfeqd	$⊢ φ \to Ⅎ y D = F$
31	24 30	nfimd	$⊢ φ \to Ⅎ y ((E \in B \land χ) \to D = F)$
32	31	adantr	$⊢ (φ \land A \in V) \to Ⅎ y ((E \in B \land χ) \to D = F)$
33	11 18 19 21 22 32	vtocldf	$⊢ (φ \land A \in V) \to ((E \in B \land χ) \to D = F)$
34	11 12 33	mp2and	$⊢ (φ \land A \in V) \to D = F$
35	10 34	sylan2	$⊢ (φ \land A \in V) \to D = F$

Metamath Proof Explorer

Theorem riotasv2d

Proof