Metamath Proof Explorer
Description: Intersection with class abstraction and equivalent wff's. (Contributed by Peter Mazsa, 21-Jul-2021)
|
|
Ref |
Expression |
|
Hypotheses |
abeqinbi.1 |
⊢ 𝐴 = ( 𝐵 ∩ 𝐶 ) |
|
|
abeqinbi.2 |
⊢ 𝐵 = { 𝑥 ∣ 𝜑 } |
|
|
abeqinbi.3 |
⊢ ( 𝑥 ∈ 𝐶 → ( 𝜑 ↔ 𝜓 ) ) |
|
Assertion |
abeqinbi |
⊢ 𝐴 = { 𝑥 ∈ 𝐶 ∣ 𝜓 } |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
abeqinbi.1 |
⊢ 𝐴 = ( 𝐵 ∩ 𝐶 ) |
2 |
|
abeqinbi.2 |
⊢ 𝐵 = { 𝑥 ∣ 𝜑 } |
3 |
|
abeqinbi.3 |
⊢ ( 𝑥 ∈ 𝐶 → ( 𝜑 ↔ 𝜓 ) ) |
4 |
1 2
|
abeqin |
⊢ 𝐴 = { 𝑥 ∈ 𝐶 ∣ 𝜑 } |
5 |
4 3
|
rabimbieq |
⊢ 𝐴 = { 𝑥 ∈ 𝐶 ∣ 𝜓 } |