Metamath Proof Explorer
Description: Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016)
|
|
Ref |
Expression |
|
Hypotheses |
elabreximdv.1 |
⊢ ( 𝐴 = 𝐵 → ( 𝜒 ↔ 𝜓 ) ) |
|
|
elabreximdv.2 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
|
|
elabreximdv.3 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝜓 ) |
|
Assertion |
elabreximdv |
⊢ ( ( 𝜑 ∧ 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 } ) → 𝜒 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
elabreximdv.1 |
⊢ ( 𝐴 = 𝐵 → ( 𝜒 ↔ 𝜓 ) ) |
2 |
|
elabreximdv.2 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
3 |
|
elabreximdv.3 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝜓 ) |
4 |
|
nfv |
⊢ Ⅎ 𝑥 𝜑 |
5 |
|
nfv |
⊢ Ⅎ 𝑥 𝜒 |
6 |
4 5 1 2 3
|
elabreximd |
⊢ ( ( 𝜑 ∧ 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 } ) → 𝜒 ) |