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 
|- { x e. A | x e. B } = { x e. B | x e. A }

Proof

Step Hyp Ref Expression
1 ancom 
 |-  ( ( x e. A /\ x e. B ) <-> ( x e. B /\ x e. A ) )
2 1 rabbia2 
 |-  { x e. A | x e. B } = { x e. B | x e. A }