Metamath Proof Explorer
Description: Swap with a membership relation in a restricted class abstraction.
(Contributed by NM, 4-Jul-2005)
|
|
Ref |
Expression |
|
Assertion |
rabswap |
⊢ { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵 } = { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴 } |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
ancom |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) |
2 |
1
|
rabbia2 |
⊢ { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵 } = { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴 } |