Metamath Proof Explorer

Table of Contents - 2.1.5. Restricted quantification

Restricted universal and existential quantification
1. wral
2. df-ral
3. rgen
4. ralel
5. rgenw
6. rgen2w
7. mprg
8. mprgbir
9. raln
10. wrex
11. df-rex
12. ralnex
13. dfrex2
14. nrex
15. alral
16. rexex
17. rextru
18. ralimi2
19. reximi2
20. ralimia
21. reximia
22. ralimiaa
23. ralimi
24. reximi
25. ral2imi
26. ralim
27. rexim
28. reximiaOLD
29. ralbii2
30. rexbii2
31. ralbiia
32. rexbiia
33. ralbii
34. rexbii
35. ralanid
36. rexanid
37. ralcom3
38. ralcom3OLD
39. dfral2
40. rexnal
41. ralinexa
42. rexanali
43. ralbi
44. rexbi
45. rexbiOLD
46. ralrexbid
47. ralrexbidOLD
48. r19.35
49. r19.35OLD
50. r19.26m
51. r19.26
52. r19.26-3
53. ralbiim
54. r19.29
55. r19.29OLD
56. r19.29r
57. r19.29rOLD
58. r19.29imd
59. r19.40
60. r19.30
61. r19.30OLD
62. r19.43
63. 2ralimi
64. 3ralimi
65. 4ralimi
66. 5ralimi
67. 6ralimi
68. 2ralbii
69. 2rexbii
70. 3ralbii
71. 4ralbii
72. 2ralbiim
73. ralnex2
74. ralnex3
75. rexnal2
76. rexnal3
77. nrexralim
78. r19.26-2
79. 2r19.29
80. r19.29d2r
81. r19.29d2rOLD
82. r2allem
83. r2exlem
84. hbralrimi
85. ralrimiv
86. ralrimiva
87. rexlimiva
88. rexlimiv
89. nrexdv
90. ralrimivw
91. rexlimivw
92. ralrimdv
93. rexlimdv
94. ralrimdva
95. rexlimdva
96. rexlimdvaa
97. rexlimdva2
98. r19.29an
99. rexlimdv3a
100. rexlimdvw
101. rexlimddv
102. r19.29a
103. ralimdv2
104. reximdv2
105. reximdvai
106. reximdvaiOLD
107. ralimdva
108. reximdva
109. ralimdv
110. reximdv
111. reximddv
112. reximssdv
113. ralbidv2
114. rexbidv2
115. ralbidva
116. rexbidva
117. ralbidv
118. rexbidv
119. r19.21v
120. r19.21vOLD
121. r19.37v
122. r19.23v
123. r19.36v
124. rexlimivOLD
125. rexlimivaOLD
126. rexlimivwOLD
127. r19.27v
128. r19.41v
129. r19.28v
130. r19.42v
131. r19.32v
132. r19.45v
133. r19.44v
134. r2al
135. r2ex
136. r3al
137. rgen2
138. ralrimivv
139. rexlimivv
140. ralrimivva
141. ralrimdvv
142. rgen3
143. ralrimivvva
144. ralimdvva
145. reximdvva
146. ralimdvv
147. ralimd4v
148. ralimd6v
149. ralrimdvva
150. rexlimdvv
151. rexlimdvva
152. reximddv2
153. r19.29vva
154. r19.29vvaOLD
155. 2rexbiia
156. 2ralbidva
157. 2rexbidva
158. 2ralbidv
159. 2rexbidv
160. rexralbidv
161. 3ralbidv
162. 4ralbidv
163. 6ralbidv
164. r19.41vv
165. reeanlem
166. reeanv
167. 3reeanv
168. 2ralor
169. 2ralorOLD
170. risset
171. nelb
172. nelbOLD
173. rspw
174. cbvralvw
175. cbvrexvw
176. cbvraldva
177. cbvrexdva
178. cbvral2vw
179. cbvrex2vw
180. cbvral3vw
181. cbvral4vw
182. cbvral6vw
183. cbvral8vw
184. rsp
185. rspa
186. rspe
187. rspec
188. r19.21bi
189. r19.21be
190. r19.21t
191. r19.21
192. r19.23t
193. r19.23
194. ralrimi
195. ralrimia
196. rexlimi
197. ralimdaa
198. reximdai
199. r19.37
200. r19.41
201. ralrimd
202. rexlimd2
203. rexlimd
204. r19.29af2
205. r19.29af
206. reximd2a
207. ralbida
208. ralbidaOLD
209. rexbida
210. ralbid
211. rexbid
212. rexbidvALT
213. rexbidvaALT
214. rsp2
215. rsp2e
216. rspec2
217. rspec3
218. r2alf
219. r2exf
220. 2ralbida
221. nfra1
222. nfre1
223. ralcom4
224. ralcom4OLD
225. rexcom4
226. ralcom
227. rexcom
228. rexcomOLD
229. rexcom4a
230. ralrot3
231. ralcom13
232. ralcom13OLD
233. rexcom13
234. rexrot4
235. 2ex2rexrot
236. nfra2w
237. nfra2wOLD
238. hbra1
239. ralcomf
240. rexcomf
241. cbvralfw
242. cbvrexfw
243. cbvralw
244. cbvrexw
245. hbral
246. nfraldw
247. nfrexdw
248. nfralw
249. nfralwOLD
250. nfrexw
251. r19.12
252. r19.12OLD
253. reean
254. cbvralsvw
255. cbvrexsvw
256. cbvralsvwOLD
257. cbvrexsvwOLD
258. nfraldwOLD
259. nfra2wOLDOLD
260. cbvralfwOLD
261. rexeq
262. raleq
263. raleqi
264. rexeqi
265. raleqdv
266. rexeqdv
267. raleqbidva
268. rexeqbidva
269. raleqbidvv
270. raleqbidvvOLD
271. rexeqbidvv
272. rexeqbidvvOLD
273. raleqbi1dv
274. rexeqbi1dv
275. raleqOLD
276. rexeqOLD
277. raleleq
278. raleqbii
279. rexeqbii
280. raleleqOLD
281. raleleqALT
282. raleqbidv
283. rexeqbidv
284. cbvraldva2
285. cbvrexdva2
286. cbvrexdva2OLD
287. cbvraldvaOLD
288. cbvrexdvaOLD
289. raleqf
290. rexeqf
291. rexeqfOLD
292. raleqbid
293. rexeqbid
294. sbralie
295. sbralieALT
296. cbvralf
297. cbvrexf
298. cbvral
299. cbvrex
300. cbvralv
301. cbvrexv
302. cbvralsv
303. cbvrexsv
304. cbvral2v
305. cbvrex2v
306. cbvral3v
307. rgen2a
308. nfrald
309. nfrexd
310. nfral
311. nfrex
312. nfra2
313. ralcom2
Restricted existential uniqueness and at-most-one quantifier
1. wreu
2. wrmo
3. df-rmo
4. df-reu
5. reu5
6. reurmo
7. reurex
8. mormo
9. rmobiia
10. reubiia
11. rmobii
12. reubii
13. rmoanid
14. reuanid
15. rmoanidOLD
16. reuanidOLD
17. 2reu2rex
18. rmobidva
19. reubidva
20. rmobidv
21. reubidv
22. reueubd
23. rmo5
24. nrexrmo
25. moel
26. cbvrmovw
27. cbvreuvw
28. moelOLD
29. rmobida
30. reubida
31. rmobidvaOLD
32. cbvrmow
33. cbvreuw
34. nfrmo1
35. nfreu1
36. nfrmow
37. nfreuw
38. cbvrmowOLD
39. cbvreuwOLD
40. cbvreuvwOLD
41. rmoeq1
42. reueq1
43. rmoeq1OLD
44. reueq1OLD
45. rmoeqd
46. reueqd
47. rmoeq1f
48. reueq1f
49. nfreuwOLD
50. nfrmowOLD
51. cbvreu
52. cbvrmo
53. cbvrmov
54. cbvreuv
55. nfrmod
56. nfreud
57. nfrmo
58. nfreu
Restricted class abstraction
1. crab
2. df-rab
3. rabbidva2
4. rabbia2
5. rabbiia
6. rabbiiaOLD
7. rabbii
8. rabbidva
9. rabbidv
10. rabbieq
11. rabswap
12. cbvrabv
13. rabeqcda
14. rabeqc
15. rabeqi
16. rabeq
17. rabeqdv
18. rabeqbidva
19. rabeqbidv
20. rabrabi
21. nfrab1
22. rabid
23. rabidim1
24. reqabi
25. rabrab
26. rabrabiOLD
27. rabbida4
28. rabbida
29. rabbid
30. rabeqd
31. rabeqbida
32. rabbi
33. rabid2f
34. rabid2
35. rabid2OLD
36. rabeqf
37. cbvrabw
38. nfrabw
39. nfrabwOLD
40. rabbidaOLD
41. rabeqiOLD
42. nfrab
43. cbvrab