Theorem cnvcnv

Description: The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003) (Proof shortened by BJ, 26-Nov-2021)

	Ref	Expression
Assertion	cnvcnv	⊢ ◡ ◡ 𝐴 = ( 𝐴 ∩ ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		cnvin	⊢ ◡ ( ◡ 𝐴 ∩ ◡ ( V × V ) ) = ( ◡ ◡ 𝐴 ∩ ◡ ◡ ( V × V ) )
2		cnvin	⊢ ◡ ( 𝐴 ∩ ( V × V ) ) = ( ◡ 𝐴 ∩ ◡ ( V × V ) )
3	2	cnveqi	⊢ ◡ ◡ ( 𝐴 ∩ ( V × V ) ) = ◡ ( ◡ 𝐴 ∩ ◡ ( V × V ) )
4		relcnv	⊢ Rel ◡ ◡ 𝐴
5		df-rel	⊢ ( Rel ◡ ◡ 𝐴 ↔ ◡ ◡ 𝐴 ⊆ ( V × V ) )
6	4 5	mpbi	⊢ ◡ ◡ 𝐴 ⊆ ( V × V )
7		relxp	⊢ Rel ( V × V )
8		dfrel2	⊢ ( Rel ( V × V ) ↔ ◡ ◡ ( V × V ) = ( V × V ) )
9	7 8	mpbi	⊢ ◡ ◡ ( V × V ) = ( V × V )
10	6 9	sseqtrri	⊢ ◡ ◡ 𝐴 ⊆ ◡ ◡ ( V × V )
11		dfss	⊢ ( ◡ ◡ 𝐴 ⊆ ◡ ◡ ( V × V ) ↔ ◡ ◡ 𝐴 = ( ◡ ◡ 𝐴 ∩ ◡ ◡ ( V × V ) ) )
12	10 11	mpbi	⊢ ◡ ◡ 𝐴 = ( ◡ ◡ 𝐴 ∩ ◡ ◡ ( V × V ) )
13	1 3 12	3eqtr4ri	⊢ ◡ ◡ 𝐴 = ◡ ◡ ( 𝐴 ∩ ( V × V ) )
14		relinxp	⊢ Rel ( 𝐴 ∩ ( V × V ) )
15		dfrel2	⊢ ( Rel ( 𝐴 ∩ ( V × V ) ) ↔ ◡ ◡ ( 𝐴 ∩ ( V × V ) ) = ( 𝐴 ∩ ( V × V ) ) )
16	14 15	mpbi	⊢ ◡ ◡ ( 𝐴 ∩ ( V × V ) ) = ( 𝐴 ∩ ( V × V ) )
17	13 16	eqtri	⊢ ◡ ◡ 𝐴 = ( 𝐴 ∩ ( V × V ) )