Description: Substituting into equivalent wff's gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018) (Proof shortened by Wolf Lammen, 4-May-2023) Avoid ax-10, ax-12. (Revised by Steven Nguyen, 5-May-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sbcbi2 | ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abbi1 | ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ) | |
| 2 | eleq2 | ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝐴 ∈ { 𝑥 ∣ 𝜓 } ) ) | |
| 3 | 1 2 | syl | ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝐴 ∈ { 𝑥 ∣ 𝜓 } ) ) |
| 4 | df-sbc | ⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } ) | |
| 5 | df-sbc | ⊢ ( [ 𝐴 / 𝑥 ] 𝜓 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜓 } ) | |
| 6 | 3 4 5 | 3bitr4g | ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜓 ) ) |