Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Proper substitution of classes for sets into classes
csbief
Metamath Proof Explorer
Description: Conversion of implicit substitution to explicit substitution into a
class. (Contributed by NM , 26-Nov-2005) (Revised by Mario Carneiro , 13-Oct-2016)

Ref
Expression
Hypotheses
csbief.1
⊢ 𝐴 ∈ V
csbief.2
⊢ Ⅎ 𝑥 𝐶
csbief.3
⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
Assertion
csbief
⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶

Proof
Step
Hyp
Ref
Expression
1
csbief.1
⊢ 𝐴 ∈ V
2
csbief.2
⊢ Ⅎ 𝑥 𝐶
3
csbief.3
⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
4
2
a1i
⊢ ( 𝐴 ∈ V → Ⅎ 𝑥 𝐶 )
5
4 3
csbiegf
⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶 )
6
1 5
ax-mp
⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶