MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nqereu Unicode version

Theorem nqereu 9328
Description: There is a unique element of equivalent to each element of X. . (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
Assertion
Ref Expression
nqereu
Distinct variable group:   ,

Proof of Theorem nqereu
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp2 5022 . . 3
2 pion 9278 . . . . . . . . 9
3 suceloni 6648 . . . . . . . . 9
42, 3syl 16 . . . . . . . 8
5 vex 3112 . . . . . . . . 9
65sucid 4962 . . . . . . . 8
7 eleq2 2530 . . . . . . . . 9
87rspcev 3210 . . . . . . . 8
94, 6, 8sylancl 662 . . . . . . 7
109adantl 466 . . . . . 6
11 elequ2 1823 . . . . . . . . . . . . . 14
1211imbi1d 317 . . . . . . . . . . . . 13
13122ralbidv 2901 . . . . . . . . . . . 12
14 opeq1 4217 . . . . . . . . . . . . . . . . . . 19
1514breq2d 4464 . . . . . . . . . . . . . . . . . 18
1615rexbidv 2968 . . . . . . . . . . . . . . . . 17
1716imbi2d 316 . . . . . . . . . . . . . . . 16
18 elequ1 1821 . . . . . . . . . . . . . . . . 17
19 opeq2 4218 . . . . . . . . . . . . . . . . . . 19
2019breq2d 4464 . . . . . . . . . . . . . . . . . 18
2120rexbidv 2968 . . . . . . . . . . . . . . . . 17
2218, 21imbi12d 320 . . . . . . . . . . . . . . . 16
2317, 22cbvral2v 3092 . . . . . . . . . . . . . . 15
2423ralbii 2888 . . . . . . . . . . . . . 14
25 rexnal 2905 . . . . . . . . . . . . . . . . . . 19
26 pm4.63 421 . . . . . . . . . . . . . . . . . . . . 21
27 xp2nd 6831 . . . . . . . . . . . . . . . . . . . . . . . 24
28 ltpiord 9286 . . . . . . . . . . . . . . . . . . . . . . . . 25
2928ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . 24
3027, 29sylan2 474 . . . . . . . . . . . . . . . . . . . . . . 23
3130adantll 713 . . . . . . . . . . . . . . . . . . . . . 22
3231anbi2d 703 . . . . . . . . . . . . . . . . . . . . 21
3326, 32syl5bb 257 . . . . . . . . . . . . . . . . . . . 20
3433rexbidva 2965 . . . . . . . . . . . . . . . . . . 19
3525, 34syl5bbr 259 . . . . . . . . . . . . . . . . . 18
36 xp1st 6830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
37 elequ2 1823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3837imbi1d 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
39382ralbidv 2901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
4039rspccv 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
41 opeq1 4217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4241breq2d 4464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
4342rexbidv 2968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4443imbi2d 316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
4544ralbidv 2896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4645rspccv 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
47 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
48 opeq2 4218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
4948breq2d 4464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
5049rexbidv 2968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5147, 50imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5251rspccv 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5346, 52syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
5440, 53syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
5554imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5636, 55syl5 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5727, 56mpdi 42 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
58573imp 1190 . . . . . . . . . . . . . . . . . . . . . . . . . 26
59 1st2nd2 6837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6059breq2d 4464 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6160rexbidv 2968 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
62613ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6358, 62mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . 25
64 enqer 9320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6564a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
66 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6865, 66, 67ertr4d 7349 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6968ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7069reximdv 2931 . . . . . . . . . . . . . . . . . . . . . . . . 25
7163, 70syl5com 30 . . . . . . . . . . . . . . . . . . . . . . . 24
72713expia 1198 . . . . . . . . . . . . . . . . . . . . . . 23
7372com23 78 . . . . . . . . . . . . . . . . . . . . . 22
7473impd 431 . . . . . . . . . . . . . . . . . . . . 21
7574rexlimdva 2949 . . . . . . . . . . . . . . . . . . . 20
7675ex 434 . . . . . . . . . . . . . . . . . . 19
7776com3r 79 . . . . . . . . . . . . . . . . . 18
7835, 77syl6bi 228 . . . . . . . . . . . . . . . . 17
7978com13 80 . . . . . . . . . . . . . . . 16
80 mulcompi 9295 . . . . . . . . . . . . . . . . . . . 20
81 enqbreq 9318 . . . . . . . . . . . . . . . . . . . . 21
8281anidms 645 . . . . . . . . . . . . . . . . . . . 20
8380, 82mpbiri 233 . . . . . . . . . . . . . . . . . . 19
84 opelxpi 5036 . . . . . . . . . . . . . . . . . . . 20
85 breq1 4455 . . . . . . . . . . . . . . . . . . . . . . . 24
86 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8786, 5op2ndd 6811 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8887breq2d 4464 . . . . . . . . . . . . . . . . . . . . . . . . 25
8988notbid 294 . . . . . . . . . . . . . . . . . . . . . . . 24
9085, 89imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . 23
9190ralbidv 2896 . . . . . . . . . . . . . . . . . . . . . 22
92 df-nq 9311 . . . . . . . . . . . . . . . . . . . . . 22
9391, 92elrab2 3259 . . . . . . . . . . . . . . . . . . . . 21
9493simplbi2 625 . . . . . . . . . . . . . . . . . . . 20
9584, 94syl 16 . . . . . . . . . . . . . . . . . . 19
96 breq1 4455 . . . . . . . . . . . . . . . . . . . . 21
9796rspcev 3210 . . . . . . . . . . . . . . . . . . . 20
9897expcom 435 . . . . . . . . . . . . . . . . . . 19
9983, 95, 98sylsyld 56 . . . . . . . . . . . . . . . . . 18
10099com12 31 . . . . . . . . . . . . . . . . 17
101100a1dd 46 . . . . . . . . . . . . . . . 16
10279, 101pm2.61d2 160 . . . . . . . . . . . . . . 15
103102ralrimivv 2877 . . . . . . . . . . . . . 14
10424, 103sylbir 213 . . . . . . . . . . . . 13
105104a1i 11 . . . . . . . . . . . 12
10613, 105tfis2 6691 . . . . . . . . . . 11
107 rsp 2823 . . . . . . . . . . 11
108106, 107syl 16 . . . . . . . . . 10
109 rsp 2823 . . . . . . . . . 10
110108, 109syl6 33 . . . . . . . . 9
111110impd 431 . . . . . . . 8
112111com12 31 . . . . . . 7
113112rexlimdv 2947 . . . . . 6
11410, 113mpd 15 . . . . 5
115 breq2 4456 . . . . . 6
116115rexbidv 2968 . . . . 5
117114, 116syl5ibrcom 222 . . . 4
118117rexlimivv 2954 . . 3
1191, 118sylbi 195 . 2
120 breq2 4456 . . . . . 6
121 breq2 4456 . . . . . 6
122120, 121anbi12d 710 . . . . 5
123122imbi1d 317 . . . 4
1241232ralbidv 2901 . . 3
12564a1i 11 . . . . . 6
126 simpl 457 . . . . . 6
127 simpr 461 . . . . . 6
128125, 126, 127ertr4d 7349 . . . . 5
129 mulcompi 9295 . . . . . . . . . . 11
130 elpqn 9324 . . . . . . . . . . . . . . 15
131 breq1 4455 . . . . . . . . . . . . . . . . . . 19
132 fveq2 5871 . . . . . . . . . . . . . . . . . . . . 21
133132breq2d 4464 . . . . . . . . . . . . . . . . . . . 20
134133notbid 294 . . . . . . . . . . . . . . . . . . 19
135131, 134imbi12d 320 . . . . . . . . . . . . . . . . . 18
136135ralbidv 2896 . . . . . . . . . . . . . . . . 17
137136, 92elrab2 3259 . . . . . . . . . . . . . . . 16
138137simprbi 464 . . . . . . . . . . . . . . 15
139 breq2 4456 . . . . . . . . . . . . . . . . 17
140 fveq2 5871 . . . . . . . . . . . . . . . . . . 19
141140breq1d 4462 . . . . . . . . . . . . . . . . . 18
142141notbid 294 . . . . . . . . . . . . . . . . 17
143139, 142imbi12d 320 . . . . . . . . . . . . . . . 16
144143rspcva 3208 . . . . . . . . . . . . . . 15
145130, 138, 144syl2anr 478 . . . . . . . . . . . . . 14
146145imp 429 . . . . . . . . . . . . 13
14764a1i 11 . . . . . . . . . . . . . . . . . 18
148 id 22 . . . . . . . . . . . . . . . . . 18
149147, 148ersym 7342 . . . . . . . . . . . . . . . . 17
150 elpqn 9324 . . . . . . . . . . . . . . . . . 18
15192rabeq2i 3106 . . . . . . . . . . . . . . . . . . 19
152151simprbi 464 . . . . . . . . . . . . . . . . . 18
153 breq2 4456 . . . . . . . . . . . . . . . . . . . 20
154 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . 22
155154breq1d 4462 . . . . . . . . . . . . . . . . . . . . 21
156155notbid 294 . . . . . . . . . . . . . . . . . . . 20
157153, 156imbi12d 320 . . . . . . . . . . . . . . . . . . 19
158157rspcva 3208 . . . . . . . . . . . . . . . . . 18
159150, 152, 158syl2an 477 . . . . . . . . . . . . . . . . 17
160149, 159syl5 32 . . . . . . . . . . . . . . . 16
161160imp 429 . . . . . . . . . . . . . . 15