Metamath Proof Explorer
Description: An equivalence for class substitution. (Contributed by NM, 11-Oct-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011)
|
|
Ref |
Expression |
|
Assertion |
sbc6g |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
sbc5 |
⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) |
2 |
|
alexeqg |
⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) ) |
3 |
1 2
|
bitr4id |
⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) |