Metamath Proof Explorer
Description: Convert a universal quantification restricted to a singleton to a
substitution. (Contributed by NM, 27-Apr-2009)
|
|
Ref |
Expression |
|
Hypotheses |
ralsn.1 |
⊢ 𝐴 ∈ V |
|
|
ralsn.2 |
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) |
|
Assertion |
ralsn |
⊢ ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ 𝜓 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
ralsn.1 |
⊢ 𝐴 ∈ V |
2 |
|
ralsn.2 |
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) |
3 |
2
|
ralsng |
⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ 𝜓 ) ) |
4 |
1 3
|
ax-mp |
⊢ ( ∀ 𝑥 ∈ { 𝐴 } 𝜑 ↔ 𝜓 ) |