Theorem symgmov1

Description: For a permutation of a set, each element of the set replaces an(other) element of the set. (Contributed by AV, 2-Jan-2019)

	Ref	Expression
Hypothesis	symgmov1.p	|- P = ( Base ` ( SymGrp ` N ) )
Assertion	symgmov1	|- ( Q e. P -> A. n e. N E. k e. N ( Q ` n ) = k )

Proof

Step	Hyp	Ref	Expression
1		symgmov1.p	|- P = ( Base ` ( SymGrp ` N ) )
2		eqid	|- ( SymGrp ` N ) = ( SymGrp ` N )
3	2 1	symgfv	|- ( ( Q e. P /\ n e. N ) -> ( Q ` n ) e. N )
4		clel5	|- ( ( Q ` n ) e. N <-> E. k e. N ( Q ` n ) = k )
5	3 4	sylib	|- ( ( Q e. P /\ n e. N ) -> E. k e. N ( Q ` n ) = k )
6	5	ralrimiva	|- ( Q e. P -> A. n e. N E. k e. N ( Q ` n ) = k )