This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem csbgfi

Description: Substitution for a variable not free in a class does not affect it, in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019)

Ref Expression
Hypotheses csbgfi.1 ⊢ A ∈ V
csbgfi.2 ⊢ Ⅎ _ x B
Assertion csbgfi ⊢ ⦋ A / x⦌ B = B

Proof

Step Hyp Ref Expression
1 csbgfi.1 ⊢ A ∈ V
2 csbgfi.2 ⊢ Ⅎ _ x B
3 df-csb ⊢ ⦋ A / x⦌ B = y | [˙A / x]˙ y ∈ B
4 3 eqabri ⊢ y ∈ ⦋ A / x⦌ B ↔ [˙A / x]˙ y ∈ B
5 2 nfcri ⊢ Ⅎ x y ∈ B
6 1 5 sbcgfi ⊢ [˙A / x]˙ y ∈ B ↔ y ∈ B
7 4 6 bitri ⊢ y ∈ ⦋ A / x⦌ B ↔ y ∈ B
8 7 eqriv ⊢ ⦋ A / x⦌ B = B