Metamath Proof Explorer
Description: Equality inference for restricted universal quantifier. (Contributed by Paul Chapman, 22-Jun-2011)
|
|
Ref |
Expression |
|
Hypothesis |
raleq1i.1 |
⊢ 𝐴 = 𝐵 |
|
Assertion |
raleqi |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐵 𝜑 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
raleq1i.1 |
⊢ 𝐴 = 𝐵 |
2 |
|
raleq |
⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐵 𝜑 ) ) |
3 |
1 2
|
ax-mp |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐵 𝜑 ) |