Theorem riotasv2s

Description: The value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 ) in the form of a substitution instance. Special case of riota2f . (Contributed by NM, 3-Mar-2013) (Proof shortened by Mario Carneiro, 6-Dec-2016)

	Ref	Expression
Hypothesis	riotasv2s.2	$$⊢D=\left(\iota x\in A|\forall y\in B\left(\phi \to x=C\right)\right)$$
Assertion	riotasv2s	$$⊢\left(A\in V\wedge D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)\to D=⦋E/y⦌C$$

Proof

Step	Hyp	Ref	Expression
1		riotasv2s.2	$$⊢D=\left(\iota x\in A|\forall y\in B\left(\phi \to x=C\right)\right)$$
2		3simpc	$$⊢\left(A\in V\wedge D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)\to \left(D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)$$
3		simp1	$$⊢\left(A\in V\wedge D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)\to A\in V$$
4		nfra1	$$⊢Ⅎy\forall y\in B\left(\phi \to x=C\right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
6	4 5	nfriota	$$⊢\underset{\_}{Ⅎ}y\left(\iota x\in A|\forall y\in B\left(\phi \to x=C\right)\right)$$
7	1 6	nfcxfr	$$⊢\underset{\_}{Ⅎ}yD$$
8	7	nfel1	$$⊢ℲyD\in A$$
9		nfv	$$⊢ℲyE\in B$$
10		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi$$
11	9 10	nfan	$$⊢Ⅎy\left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)$$
12	8 11	nfan	$$⊢Ⅎy\left(D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)$$
13		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋E/y⦌C$$
14	13	a1i	$$⊢\left(D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)\to \underset{\_}{Ⅎ}y⦋E/y⦌C$$
15	10	a1i	$$⊢\left(D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)\to Ⅎy\underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi$$
16	1	a1i	$$⊢\left(D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)\to D=\left(\iota x\in A|\forall y\in B\left(\phi \to x=C\right)\right)$$
17		sbceq1a	$$⊢y=E\to \left(\phi \leftrightarrow \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)$$
18	17	adantl	$$⊢\left(\left(D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)\wedge y=E\right)\to \left(\phi \leftrightarrow \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)$$
19		csbeq1a	$$⊢y=E\to C=⦋E/y⦌C$$
20	19	adantl	$$⊢\left(\left(D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)\wedge y=E\right)\to C=⦋E/y⦌C$$
21		simpl	$$⊢\left(D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)\to D\in A$$
22		simprl	$$⊢\left(D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)\to E\in B$$
23		simprr	$$⊢\left(D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)\to \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi$$
24	12 14 15 16 18 20 21 22 23	riotasv2d	$$⊢\left(\left(D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)\wedge A\in V\right)\to D=⦋E/y⦌C$$
25	2 3 24	syl2anc	$$⊢\left(A\in V\wedge D\in A\wedge \left(E\in B\wedge \underset{\dot{}}{[}E/y\underset{\dot{}}{]}\phi \right)\right)\to D=⦋E/y⦌C$$