Theorem cnvsymOLD

Description: Obsolete version of cnvsym as of 29-Dec-2024. (Contributed by NM, 28-Dec-1996) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by SN, 23-Dec-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	cnvsymOLD	|- ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )

Proof

Step	Hyp	Ref	Expression
1		relcnv	|- Rel `' R
2		ssrel3	|- ( Rel `' R -> ( `' R C_ R <-> A. y A. x ( y `' R x -> y R x ) ) )
3	1 2	ax-mp	|- ( `' R C_ R <-> A. y A. x ( y `' R x -> y R x ) )
4		alcom	|- ( A. y A. x ( y `' R x -> y R x ) <-> A. x A. y ( y `' R x -> y R x ) )
5		vex	|- y e. _V
6		vex	|- x e. _V
7	5 6	brcnv	|- ( y `' R x <-> x R y )
8	7	imbi1i	|- ( ( y `' R x -> y R x ) <-> ( x R y -> y R x ) )
9	8	2albii	|- ( A. x A. y ( y `' R x -> y R x ) <-> A. x A. y ( x R y -> y R x ) )
10	3 4 9	3bitri	|- ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )