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 Gino Giotto, 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↔zy[˙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 ⊢zy[˙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 ⊢φ→∀zz∈y|[˙A/x]˙y∈B↔z∈C
15 dfcleq ⊢y|[˙A/x]˙y∈B=C↔∀zz∈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