Theorem rabswap

Description: Swap with a membership relation in a restricted class abstraction. (Contributed by NM, 4-Jul-2005)

	Ref	Expression
Assertion	rabswap	$$⊢\left\{x\in A|x\in B\right\}=\left\{x\in B|x\in A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ancom	$$⊢\left(x\in A\wedge x\in B\right)\leftrightarrow \left(x\in B\wedge x\in A\right)$$
2	1	rabbia2	$$⊢\left\{x\in A|x\in B\right\}=\left\{x\in B|x\in A\right\}$$