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	$⊢ \{x \in A \| x \in B\} = \{x \in B \| x \in A\}$

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