Theorem cnvcnvsn

Description: Double converse of a singleton of an ordered pair. (Unlike cnvsn , this does not need any sethood assumptions on A and B .) (Contributed by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	cnvcnvsn	|- `' `' { <. A , B >. } = `' { <. B , A >. }

Proof

Step	Hyp	Ref	Expression
1		relcnv	|- Rel `' `' { <. A , B >. }
2		relcnv	|- Rel `' { <. B , A >. }
3		vex	|- x e. _V
4		vex	|- y e. _V
5	3 4	opelcnv	|- ( <. x , y >. e. `' `' { <. A , B >. } <-> <. y , x >. e. `' { <. A , B >. } )
6		ancom	|- ( ( x = A /\ y = B ) <-> ( y = B /\ x = A ) )
7	3 4	opth	|- ( <. x , y >. = <. A , B >. <-> ( x = A /\ y = B ) )
8	4 3	opth	|- ( <. y , x >. = <. B , A >. <-> ( y = B /\ x = A ) )
9	6 7 8	3bitr4i	|- ( <. x , y >. = <. A , B >. <-> <. y , x >. = <. B , A >. )
10		opex	|- <. x , y >. e. _V
11	10	elsn	|- ( <. x , y >. e. { <. A , B >. } <-> <. x , y >. = <. A , B >. )
12		opex	|- <. y , x >. e. _V
13	12	elsn	|- ( <. y , x >. e. { <. B , A >. } <-> <. y , x >. = <. B , A >. )
14	9 11 13	3bitr4i	|- ( <. x , y >. e. { <. A , B >. } <-> <. y , x >. e. { <. B , A >. } )
15	4 3	opelcnv	|- ( <. y , x >. e. `' { <. A , B >. } <-> <. x , y >. e. { <. A , B >. } )
16	3 4	opelcnv	|- ( <. x , y >. e. `' { <. B , A >. } <-> <. y , x >. e. { <. B , A >. } )
17	14 15 16	3bitr4i	|- ( <. y , x >. e. `' { <. A , B >. } <-> <. x , y >. e. `' { <. B , A >. } )
18	5 17	bitri	|- ( <. x , y >. e. `' `' { <. A , B >. } <-> <. x , y >. e. `' { <. B , A >. } )
19	1 2 18	eqrelriiv	|- `' `' { <. A , B >. } = `' { <. B , A >. }