This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ι x ∈ A | ∀ y ∈ B φ → x = C
Assertion riotasv2s ⊢ A ∈ V ∧ D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ → D = ⦋ E / y⦌ C

Proof

Step Hyp Ref Expression
1 riotasv2s.2 ⊢ D = ι x ∈ A | ∀ y ∈ B φ → x = C
2 3simpc ⊢ A ∈ V ∧ D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ → D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ
3 simp1 ⊢ A ∈ V ∧ D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ → A ∈ V
4 nfra1 ⊢ Ⅎ y ∀ y ∈ B φ → x = C
5 nfcv ⊢ Ⅎ _ y A
6 4 5 nfriota ⊢ Ⅎ _ y ι x ∈ A | ∀ y ∈ B φ → x = C
7 1 6 nfcxfr ⊢ Ⅎ _ y D
8 7 nfel1 ⊢ Ⅎ y D ∈ A
9 nfv ⊢ Ⅎ y E ∈ B
10 nfsbc1v ⊢ Ⅎ y [˙E / y]˙ φ
11 9 10 nfan ⊢ Ⅎ y E ∈ B ∧ [˙E / y]˙ φ
12 8 11 nfan ⊢ Ⅎ y D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ
13 nfcsb1v ⊢ Ⅎ _ y ⦋ E / y⦌ C
14 13 a1i ⊢ D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ → Ⅎ _ y ⦋ E / y⦌ C
15 10 a1i ⊢ D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ → Ⅎ y [˙E / y]˙ φ
16 1 a1i ⊢ D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ → D = ι x ∈ A | ∀ y ∈ B φ → x = C
17 sbceq1a ⊢ y = E → φ ↔ [˙E / y]˙ φ
18 17 adantl ⊢ D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ ∧ y = E → φ ↔ [˙E / y]˙ φ
19 csbeq1a ⊢ y = E → C = ⦋ E / y⦌ C
20 19 adantl ⊢ D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ ∧ y = E → C = ⦋ E / y⦌ C
21 simpl ⊢ D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ → D ∈ A
22 simprl ⊢ D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ → E ∈ B
23 simprr ⊢ D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ → [˙E / y]˙ φ
24 12 14 15 16 18 20 21 22 23 riotasv2d ⊢ D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ ∧ A ∈ V → D = ⦋ E / y⦌ C
25 2 3 24 syl2anc ⊢ A ∈ V ∧ D ∈ A ∧ E ∈ B ∧ [˙E / y]˙ φ → D = ⦋ E / y⦌ C