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, 26-Jan-2013) (Proof shortened by Mario Carneiro, 6-Dec-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | riotasv.1 | ⊢ 𝐴 ∈ V | |
| riotasv.2 | ⊢ 𝐷 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) | ||
| Assertion | riotasv | ⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → 𝐷 = 𝐶 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | riotasv.1 | ⊢ 𝐴 ∈ V | |
| 2 | riotasv.2 | ⊢ 𝐷 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) | |
| 3 | 2 | a1i | ⊢ ( 𝐷 ∈ 𝐴 → 𝐷 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) ) |
| 4 | id | ⊢ ( 𝐷 ∈ 𝐴 → 𝐷 ∈ 𝐴 ) | |
| 5 | 3 4 | riotasvd | ⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝐴 ∈ V ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → 𝐷 = 𝐶 ) ) |
| 6 | 1 5 | mpan2 | ⊢ ( 𝐷 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → 𝐷 = 𝐶 ) ) |
| 7 | 6 | 3impib | ⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → 𝐷 = 𝐶 ) |