This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) → 𝐷 = ⦋ 𝐸 / 𝑦 ⦌ 𝐶 ) |
| 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 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝐴 ∧ ( 𝐸 ∈ 𝐵 ∧ [ 𝐸 / 𝑦 ] 𝜑 ) ) → 𝐷 = ⦋ 𝐸 / 𝑦 ⦌ 𝐶 ) |