Description: A composition law for class substitution. Importantly, x may occur free in the class expression substituted for A . (Contributed by NM, 5-Sep-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | sbcco2.1 | ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 ) | |
| Assertion | sbcco2 | ⊢ ( [ 𝑥 / 𝑦 ] [ 𝐵 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbcco2.1 | ⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 ) | |
| 2 | sbsbc | ⊢ ( [ 𝑥 / 𝑦 ] [ 𝐵 / 𝑥 ] 𝜑 ↔ [ 𝑥 / 𝑦 ] [ 𝐵 / 𝑥 ] 𝜑 ) | |
| 3 | 1 | equcoms | ⊢ ( 𝑦 = 𝑥 → 𝐴 = 𝐵 ) |
| 4 | dfsbcq | ⊢ ( 𝐴 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑥 ] 𝜑 ) ) | |
| 5 | 4 | bicomd | ⊢ ( 𝐴 = 𝐵 → ( [ 𝐵 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) |
| 6 | 3 5 | syl | ⊢ ( 𝑦 = 𝑥 → ( [ 𝐵 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) |
| 7 | 6 | sbievw | ⊢ ( [ 𝑥 / 𝑦 ] [ 𝐵 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) |
| 8 | 2 7 | bitr3i | ⊢ ( [ 𝑥 / 𝑦 ] [ 𝐵 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) |