Metamath Proof Explorer
Description: Swap with a membership relation in a restricted class abstraction.
(Contributed by NM, 4Jul2005)


Ref 
Expression 

Assertion 
rabswap 
$${\u22a2}\left\{{x}\in {A}{x}\in {B}\right\}=\left\{{x}\in {B}{x}\in {A}\right\}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

ancom 
$${\u22a2}\left({x}\in {A}\wedge {x}\in {B}\right)\leftrightarrow \left({x}\in {B}\wedge {x}\in {A}\right)$$ 
2 
1

rabbia2 
$${\u22a2}\left\{{x}\in {A}{x}\in {B}\right\}=\left\{{x}\in {B}{x}\in {A}\right\}$$ 