Description: Bidirectional conversion between an implicit class substitution hypothesis x = A -> B = C and its explicit substitution equivalent. (Contributed by NM, 24-Mar-2013) (Revised by Mario Carneiro, 11-Dec-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | csbiebg.2 | ⊢ Ⅎ 𝑥 𝐶 | |
| Assertion | csbiebg | ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | csbiebg.2 | ⊢ Ⅎ 𝑥 𝐶 | |
| 2 | eqeq2 | ⊢ ( 𝑎 = 𝐴 → ( 𝑥 = 𝑎 ↔ 𝑥 = 𝐴 ) ) | |
| 3 | 2 | imbi1d | ⊢ ( 𝑎 = 𝐴 → ( ( 𝑥 = 𝑎 → 𝐵 = 𝐶 ) ↔ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ) ) |
| 4 | 3 | albidv | ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ( 𝑥 = 𝑎 → 𝐵 = 𝐶 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ) ) |
| 5 | csbeq1 | ⊢ ( 𝑎 = 𝐴 → ⦋ 𝑎 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) | |
| 6 | 5 | eqeq1d | ⊢ ( 𝑎 = 𝐴 → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 = 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 ) ) |
| 7 | vex | ⊢ 𝑎 ∈ V | |
| 8 | 7 1 | csbieb | ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑎 → 𝐵 = 𝐶 ) ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 = 𝐶 ) |
| 9 | 4 6 8 | vtoclbg | ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 ) ) |