Theorem nqerid

Description: Corollary of nqereu : the function /Q acts as the identity on members of Q. . (Contributed by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	nqerid	|- ( A e. Q. -> ( /Q ` A ) = A )

Proof

Step	Hyp	Ref	Expression
1		nqerf	|- /Q : ( N. X. N. ) --> Q.
2		ffun	|- ( /Q : ( N. X. N. ) --> Q. -> Fun /Q )
3	1 2	ax-mp	|- Fun /Q
4		elpqn	|- ( A e. Q. -> A e. ( N. X. N. ) )
5		id	|- ( A e. Q. -> A e. Q. )
6		enqer	|- ~Q Er ( N. X. N. )
7	6	a1i	|- ( A e. Q. -> ~Q Er ( N. X. N. ) )
8	7 4	erref	|- ( A e. Q. -> A ~Q A )
9		df-erq	|- /Q = ( ~Q i^i ( ( N. X. N. ) X. Q. ) )
10	9	breqi	|- ( A /Q A <-> A ( ~Q i^i ( ( N. X. N. ) X. Q. ) ) A )
11		brinxp2	|- ( A ( ~Q i^i ( ( N. X. N. ) X. Q. ) ) A <-> ( ( A e. ( N. X. N. ) /\ A e. Q. ) /\ A ~Q A ) )
12	10 11	bitri	|- ( A /Q A <-> ( ( A e. ( N. X. N. ) /\ A e. Q. ) /\ A ~Q A ) )
13	4 5 8 12	syl21anbrc	|- ( A e. Q. -> A /Q A )
14		funbrfv	|- ( Fun /Q -> ( A /Q A -> ( /Q ` A ) = A ) )
15	3 13 14	mpsyl	|- ( A e. Q. -> ( /Q ` A ) = A )