Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005) (Revised by Mario Carneiro, 23-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ralsnsg | ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ral | ⊢ ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝜑 ) ) | |
| 2 | velsn | ⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 ) | |
| 3 | 2 | imbi1i | ⊢ ( ( 𝑥 ∈ { 𝐴 } → 𝜑 ) ↔ ( 𝑥 = 𝐴 → 𝜑 ) ) |
| 4 | 3 | albii | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) |
| 5 | 1 4 | bitri | ⊢ ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) |
| 6 | sbc6g | ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) | |
| 7 | 5 6 | bitr4id | ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) |