Metamath Proof Explorer

Theorem csbie2df

Description: Conversion of implicit substitution to explicit class substitution. This version of csbiedf avoids a disjointness condition on x , A and x , D by substituting twice. Deduction form of csbie2 . (Contributed by AV, 29-Mar-2024)

Ref Expression
Hypotheses csbie2df.p ⊢ Ⅎ 𝑥 𝜑
csbie2df.c ⊢ ( 𝜑 → Ⅎ 𝑥 𝐶 )
csbie2df.d ⊢ ( 𝜑 → Ⅎ 𝑥 𝐷 )
csbie2df.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
csbie2df.1 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝐵 = 𝐶 )
csbie2df.2 ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → 𝐶 = 𝐷 )
Assertion csbie2df ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐷 )

Proof

Step Hyp Ref Expression
1 csbie2df.p ⊢ Ⅎ 𝑥 𝜑
2 csbie2df.c ⊢ ( 𝜑 → Ⅎ 𝑥 𝐶 )
3 csbie2df.d ⊢ ( 𝜑 → Ⅎ 𝑥 𝐷 )
4 csbie2df.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 csbie2df.1 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → 𝐵 = 𝐶 )
6 csbie2df.2 ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → 𝐶 = 𝐷 )
7 eqidd ⊢ ( 𝜑 → 𝐷 = 𝐷 )
8 dfsbcq ⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝐵 = 𝐷 ↔ [ 𝐴 / 𝑥 ] 𝐵 = 𝐷 ) )
9 sbceqg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐷 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )
10 9 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝜑 ) → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐷 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )
11 csbtt ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑥 𝐷 ) → ⦋ 𝐴 / 𝑥 ⦌ 𝐷 = 𝐷 )
12 3 11 sylan2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝜑 ) → ⦋ 𝐴 / 𝑥 ⦌ 𝐷 = 𝐷 )
13 12 eqeq2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝜑 ) → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐷 ) )
14 10 13 bitrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝜑 ) → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐷 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐷 ) )
15 4 14 mpancom ⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝐷 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐷 ) )
16 8 15 sylan9bb ⊢ ( ( 𝑦 = 𝐴 ∧ 𝜑 ) → ( [ 𝑦 / 𝑥 ] 𝐵 = 𝐷 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐷 ) )
17 16 pm5.74da ⊢ ( 𝑦 = 𝐴 → ( ( 𝜑 → [ 𝑦 / 𝑥 ] 𝐵 = 𝐷 ) ↔ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐷 ) ) )
18 6 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ( 𝐶 = 𝐷 ↔ 𝐷 = 𝐷 ) )
19 18 expcom ⊢ ( 𝑦 = 𝐴 → ( 𝜑 → ( 𝐶 = 𝐷 ↔ 𝐷 = 𝐷 ) ) )
20 19 pm5.74d ⊢ ( 𝑦 = 𝐴 → ( ( 𝜑 → 𝐶 = 𝐷 ) ↔ ( 𝜑 → 𝐷 = 𝐷 ) ) )
21 sbsbc ⊢ ( [ 𝑦 / 𝑥 ] 𝐵 = 𝐷 ↔ [ 𝑦 / 𝑥 ] 𝐵 = 𝐷 )
22 2 3 nfeqd ⊢ ( 𝜑 → Ⅎ 𝑥 𝐶 = 𝐷 )
23 5 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝐵 = 𝐷 ↔ 𝐶 = 𝐷 ) )
24 23 ex ⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝐵 = 𝐷 ↔ 𝐶 = 𝐷 ) ) )
25 1 22 24 sbiedw ⊢ ( 𝜑 → ( [ 𝑦 / 𝑥 ] 𝐵 = 𝐷 ↔ 𝐶 = 𝐷 ) )
26 21 25 bitr3id ⊢ ( 𝜑 → ( [ 𝑦 / 𝑥 ] 𝐵 = 𝐷 ↔ 𝐶 = 𝐷 ) )
27 26 pm5.74i ⊢ ( ( 𝜑 → [ 𝑦 / 𝑥 ] 𝐵 = 𝐷 ) ↔ ( 𝜑 → 𝐶 = 𝐷 ) )
28 17 20 27 vtoclbg ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐷 ) ↔ ( 𝜑 → 𝐷 = 𝐷 ) ) )
29 7 28 mpbiri ⊢ ( 𝐴 ∈ 𝑉 → ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐷 ) )
30 4 29 mpcom ⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐷 )