Metamath Proof Explorer
Description: Equality inference for restricted existential quantifier. (Contributed by Mario Carneiro, 23-Apr-2015)
|
|
Ref |
Expression |
|
Hypothesis |
raleq1i.1 |
⊢ 𝐴 = 𝐵 |
|
Assertion |
rexeqi |
⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐵 𝜑 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
raleq1i.1 |
⊢ 𝐴 = 𝐵 |
2 |
|
rexeq |
⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐵 𝜑 ) ) |
3 |
1 2
|
ax-mp |
⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐵 𝜑 ) |