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	⊢ 𝐷 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) )
Assertion	riotasv2s	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) → 𝐷 = ⦋ 𝐸 / 𝑦 ⦌ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		riotasv2s.2	⊢ 𝐷 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) )
2		3simpc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) → ( 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) )
3		simp1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) → 𝐴 ∈ 𝑉 )
4		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 )
5		nfcv	⊢ Ⅎ 𝑦 𝐴
6	4 5	nfriota	⊢ Ⅎ 𝑦 ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) )
7	1 6	nfcxfr	⊢ Ⅎ 𝑦 𝐷
8	7	nfel1	⊢ Ⅎ 𝑦 𝐷 ∈ 𝐴
9		nfv	⊢ Ⅎ 𝑦 𝐸 ∈ 𝐵
10		nfsbc1v	⊢ Ⅎ 𝑦 [ 𝐸 / 𝑦 ] 𝜑
11	9 10	nfan	⊢ Ⅎ 𝑦 ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 )
12	8 11	nfan	⊢ Ⅎ 𝑦 ( 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) )
13		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝐸 / 𝑦 ⦌ 𝐶
14	13	a1i	⊢ ( ( 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) → Ⅎ 𝑦 ⦋ 𝐸 / 𝑦 ⦌ 𝐶 )
15	10	a1i	⊢ ( ( 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) → Ⅎ 𝑦 [ 𝐸 / 𝑦 ] 𝜑 )
16	1	a1i	⊢ ( ( 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) → 𝐷 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )
17		sbceq1a	⊢ ( 𝑦 = 𝐸 → ( 𝜑 ↔ [ 𝐸 / 𝑦 ] 𝜑 ) )
18	17	adantl	⊢ ( ( ( 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) ∧ 𝑦 = 𝐸 ) → ( 𝜑 ↔ [ 𝐸 / 𝑦 ] 𝜑 ) )
19		csbeq1a	⊢ ( 𝑦 = 𝐸 → 𝐶 = ⦋ 𝐸 / 𝑦 ⦌ 𝐶 )
20	19	adantl	⊢ ( ( ( 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) ∧ 𝑦 = 𝐸 ) → 𝐶 = ⦋ 𝐸 / 𝑦 ⦌ 𝐶 )
21		simpl	⊢ ( ( 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) → 𝐷 ∈ 𝐴 )
22		simprl	⊢ ( ( 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) → 𝐸 ∈ 𝐵 )
23		simprr	⊢ ( ( 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) → [ 𝐸 / 𝑦 ] 𝜑 )
24	12 14 15 16 18 20 21 22 23	riotasv2d	⊢ ( ( ( 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) ∧ 𝐴 ∈ 𝑉 ) → 𝐷 = ⦋ 𝐸 / 𝑦 ⦌ 𝐶 )
25	2 3 24	syl2anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) → 𝐷 = ⦋ 𝐸 / 𝑦 ⦌ 𝐶 )