Metamath Proof Explorer


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𝑸/𝑸A=A

Proof

Step Hyp Ref Expression
1 nqerf /𝑸:𝑵×𝑵𝑸
2 ffun /𝑸:𝑵×𝑵𝑸Fun/𝑸
3 1 2 ax-mp Fun/𝑸
4 elpqn A𝑸A𝑵×𝑵
5 id A𝑸A𝑸
6 enqer ~𝑸Er𝑵×𝑵
7 6 a1i A𝑸~𝑸Er𝑵×𝑵
8 7 4 erref A𝑸A~𝑸A
9 df-erq /𝑸=~𝑸𝑵×𝑵×𝑸
10 9 breqi A/𝑸AA~𝑸𝑵×𝑵×𝑸A
11 brinxp2 A~𝑸𝑵×𝑵×𝑸AA𝑵×𝑵A𝑸A~𝑸A
12 10 11 bitri A/𝑸AA𝑵×𝑵A𝑸A~𝑸A
13 4 5 8 12 syl21anbrc A𝑸A/𝑸A
14 funbrfv Fun/𝑸A/𝑸A/𝑸A=A
15 3 13 14 mpsyl A𝑸/𝑸A=A