Metamath Proof Explorer

Theorem cgrrflx

Description: Reflexivity law for congruence. Theorem 2.1 of Schwabhauser p. 27. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion cgrrflx 
|- ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , B >. Cgr <. A , B >. )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> N e. NN )
2 simp3 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> B e. ( EE ` N ) )
3 simp2 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A e. ( EE ` N ) )
4 axcgrrflx 
 |-  ( ( N e. NN /\ B e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> <. B , A >. Cgr <. A , B >. )
5 4 3com23 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. B , A >. Cgr <. A , B >. )
6 1 2 3 3 2 3 2 5 5 cgrtr4d 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , B >. Cgr <. A , B >. )