This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rabswap

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 ⊢ { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵 } = { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴 }