Theorem refsymrel3

Description: A relation which is reflexive and symmetric (like an equivalence relation) can use the A. x e. dom R x R x version for its reflexive part, not just the A. x e. dom R A. y e. ran R ( x = y -> x R y ) version of dfrefrel3 , cf. the comment of dfrefrel3 . (Contributed by Peter Mazsa, 23-Aug-2021)

	Ref	Expression
Assertion	refsymrel3	|- ( ( RefRel R /\ SymRel R ) <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) )

Proof

Step	Hyp	Ref	Expression
1		dfrefrel3	|- ( RefRel R <-> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ Rel R ) )
2		dfsymrel3	|- ( SymRel R <-> ( A. x A. y ( x R y -> y R x ) /\ Rel R ) )
3	1 2	anbi12i	|- ( ( RefRel R /\ SymRel R ) <-> ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ Rel R ) /\ ( A. x A. y ( x R y -> y R x ) /\ Rel R ) ) )
4		anandi3r	|- ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ Rel R /\ A. x A. y ( x R y -> y R x ) ) <-> ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ Rel R ) /\ ( A. x A. y ( x R y -> y R x ) /\ Rel R ) ) )
5		3anan32	|- ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ Rel R /\ A. x A. y ( x R y -> y R x ) ) <-> ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) )
6	3 4 5	3bitr2i	|- ( ( RefRel R /\ SymRel R ) <-> ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) )
7		symrefref3	|- ( A. x A. y ( x R y -> y R x ) -> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) <-> A. x e. dom R x R x ) )
8	7	pm5.32ri	|- ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ A. x A. y ( x R y -> y R x ) ) <-> ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) )
9	8	anbi1i	|- ( ( ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) )
10	6 9	bitri	|- ( ( RefRel R /\ SymRel R ) <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) )