Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 13-Oct-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | csbiedf.1 | ⊢ Ⅎ 𝑥 𝜑 | |
csbiedf.2 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝐶 ) | ||
csbiedf.3 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | ||
csbiedf.4 | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 = 𝐶 ) | ||
Assertion | csbiedf | ⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbiedf.1 | ⊢ Ⅎ 𝑥 𝜑 | |
2 | csbiedf.2 | ⊢ ( 𝜑 → Ⅎ 𝑥 𝐶 ) | |
3 | csbiedf.3 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | |
4 | csbiedf.4 | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 = 𝐶 ) | |
5 | 4 | ex | ⊢ ( 𝜑 → ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ) |
6 | 1 5 | alrimi | ⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ) |
7 | csbiebt | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑥 𝐶 ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 ) ) | |
8 | 3 2 7 | syl2anc | ⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 ) ) |
9 | 6 8 | mpbid | ⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 ) |