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 | ⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → 𝐷 = 𝐶 ) |