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

Metamath Proof Explorer

Theorem csbied

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014) (Revised by Mario Carneiro, 13-Oct-2016) Reduce axiom usage. (Revised by GG, 15-Oct-2024)

Ref Expression
Hypotheses csbied.1 ⊢ φ → A ∈ V
csbied.2 ⊢ φ ∧ x = A → B = C
Assertion csbied ⊢ φ → ⦋ A / x⦌ B = C

Proof

Step Hyp Ref Expression
1 csbied.1 ⊢ φ → A ∈ V
2 csbied.2 ⊢ φ ∧ x = A → B = C
3 df-csb ⊢ ⦋ A / x⦌ B = y | [˙A / x]˙ y ∈ B
4 2 eleq2d ⊢ φ ∧ x = A → z ∈ B ↔ z ∈ C
5 1 4 sbcied ⊢ φ → [˙A / x]˙ z ∈ B ↔ z ∈ C
6 5 alrimiv ⊢ φ → ∀ z [˙A / x]˙ z ∈ B ↔ z ∈ C
7 df-clab ⊢ z ∈ y | [˙A / x]˙ y ∈ B ↔ z y [˙A / x]˙ y ∈ B
8 eleq1w ⊢ y = z → y ∈ B ↔ z ∈ B
9 8 sbcbidv ⊢ y = z → [˙A / x]˙ y ∈ B ↔ [˙A / x]˙ z ∈ B
10 9 sbievw ⊢ z y [˙A / x]˙ y ∈ B ↔ [˙A / x]˙ z ∈ B
11 7 10 bitr2i ⊢ [˙A / x]˙ z ∈ B ↔ z ∈ y | [˙A / x]˙ y ∈ B
12 11 bibi1i ⊢ [˙A / x]˙ z ∈ B ↔ z ∈ C ↔ z ∈ y | [˙A / x]˙ y ∈ B ↔ z ∈ C
13 12 biimpi ⊢ [˙A / x]˙ z ∈ B ↔ z ∈ C → z ∈ y | [˙A / x]˙ y ∈ B ↔ z ∈ C
14 6 13 sylg ⊢ φ → ∀ z z ∈ y | [˙A / x]˙ y ∈ B ↔ z ∈ C
15 dfcleq ⊢ y | [˙A / x]˙ y ∈ B = C ↔ ∀ z z ∈ y | [˙A / x]˙ y ∈ B ↔ z ∈ C
16 14 15 sylibr ⊢ φ → y | [˙A / x]˙ y ∈ B = C
17 3 16 eqtrid ⊢ φ → ⦋ A / x⦌ B = C