Description: This is the closest we can get to df-sbc if we start from dfsbcq (see its comments) and dfsbcq2 . (Contributed by NM, 18-Nov-2008) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sbc8g | ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfsbcq | ⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) | |
| 2 | eleq1 | ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } ) ) | |
| 3 | df-clab | ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 ) | |
| 4 | equid | ⊢ 𝑦 = 𝑦 | |
| 5 | dfsbcq2 | ⊢ ( 𝑦 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) | |
| 6 | 4 5 | ax-mp | ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) |
| 7 | 3 6 | bitr2i | ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) |
| 8 | 1 2 7 | vtoclbg | ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } ) ) |