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. ralbii2
29. rexbii2
30. ralbiia
31. rexbiia
32. ralbii
33. rexbii
34. ralanid
35. rexanid
36. ralcom3
37. ralcom3OLD
38. dfral2
39. rexnal
40. ralinexa
41. rexanali
42. ralbi
43. rexbi
44. ralrexbid
45. r19.35
46. r19.35OLD
47. r19.26m
48. r19.26
49. r19.26-3
50. ralbiim
51. r19.29
52. r19.29OLD
53. r19.29r
54. r19.29rOLD
55. r19.29imd
56. r19.40
57. r19.30
58. r19.43
59. 3r19.43
60. 2ralimi
61. 3ralimi
62. 4ralimi
63. 5ralimi
64. 6ralimi
65. 2ralbii
66. 2rexbii
67. 3ralbii
68. 4ralbii
69. 2ralbiim
70. ralnex2
71. ralnex3
72. rexnal2
73. rexnal3
74. nrexralim
75. r19.26-2
76. 2r19.29
77. r19.29d2r
78. r2allem
79. r2exlem
80. hbralrimi
81. ralrimiv
82. ralrimiva
83. rexlimiva
84. rexlimiv
85. nrexdv
86. ralrimivw
87. rexlimivw
88. ralrimdv
89. rexlimdv
90. ralrimdva
91. rexlimdva
92. rexlimdvaa
93. rexlimdva2
94. r19.29an
95. rexlimdv3a
96. rexlimdvw
97. rexlimddv
98. r19.29a
99. ralimdv2
100. reximdv2
101. reximdvai
102. ralimdva
103. reximdva
104. ralimdv
105. reximdv
106. reximddv
107. reximddv3
108. reximssdv
109. ralbidv2
110. rexbidv2
111. ralbidva
112. rexbidva
113. ralbidv
114. rexbidv
115. r19.21v
116. r19.21vOLD
117. r19.37v
118. r19.23v
119. r19.36v
120. rexlimivOLD
121. rexlimivaOLD
122. rexlimivwOLD
123. r19.27v
124. r19.41v
125. r19.28v
126. r19.42v
127. r19.32v
128. r19.45v
129. r19.44v
130. r2al
131. r2ex
132. r3al
133. r3ex
134. rgen2
135. ralrimivv
136. rexlimivv
137. ralrimivva
138. ralrimdvv
139. rgen3
140. ralrimivvva
141. ralimdvva
142. reximdvva
143. ralimdvv
144. ralimd4v
145. ralimd6v
146. ralrimdvva
147. rexlimdvv
148. rexlimdvva
149. rexlimdvvva
150. reximddv2
151. r19.29vva
152. 2rexbiia
153. 2ralbidva
154. 2rexbidva
155. 2ralbidv
156. 2rexbidv
157. rexralbidv
158. 3ralbidv
159. 4ralbidv
160. 6ralbidv
161. r19.41vv
162. reeanlem
163. reeanv
164. 3reeanv
165. 2ralor
166. 2ralorOLD
167. risset
168. nelb
169. rspw
170. cbvralvw
171. cbvrexvw
172. cbvraldva
173. cbvrexdva
174. cbvral2vw
175. cbvrex2vw
176. cbvral3vw
177. cbvral4vw
178. cbvral6vw
179. cbvral8vw
180. rsp
181. rspa
182. rspe
183. rspec
184. r19.21bi
185. r19.21be
186. r19.21t
187. r19.21
188. r19.23t
189. r19.23
190. ralrimi
191. ralrimia
192. rexlimi
193. ralimdaa
194. reximdai
195. r19.37
196. r19.41
197. ralrimd
198. rexlimd2
199. rexlimd
200. r19.29af2
201. r19.29af
202. reximd2a
203. ralbida
204. rexbida
205. ralbid
206. rexbid
207. rexbidvALT
208. rexbidvaALT
209. rsp2
210. rsp2e
211. rspec2
212. rspec3
213. r2alf
214. r2exf
215. 2ralbida
216. nfra1
217. nfre1
218. ralcom4
219. rexcom4
220. ralcom
221. rexcom
222. rexcomOLD
223. rexcom4a
224. ralrot3
225. ralcom13
226. ralcom13OLD
227. rexcom13
228. rexrot4
229. 2ex2rexrot
230. nfra2w
231. hbra1
232. ralcomf
233. rexcomf
234. cbvralfw
235. cbvrexfw
236. cbvralw
237. cbvrexw
238. hbral
239. nfraldw
240. nfrexdw
241. nfralw
242. nfralwOLD
243. nfrexw
244. r19.12
245. reean
246. cbvralsvw
247. cbvrexsvw
248. cbvralsvwOLD
249. cbvralsvwOLDOLD
250. cbvrexsvwOLD
251. rexeq
252. raleq
253. raleqi
254. rexeqi
255. raleqdv
256. rexeqdv
257. raleqtrdv
258. rexeqtrdv
259. raleqtrrdv
260. rexeqtrrdv
261. raleqbidva
262. rexeqbidva
263. raleqbidvv
264. raleqbidvvOLD
265. rexeqbidvv
266. rexeqbidvvOLD
267. raleqbi1dv
268. rexeqbi1dv
269. raleqOLD
270. rexeqOLD
271. raleleq
272. raleleqOLD
273. raleqbii
274. rexeqbii
275. raleqbidv
276. rexeqbidv
277. cbvraldva2
278. cbvrexdva2
279. cbvrexdva2OLD
280. cbvraldvaOLD
281. cbvrexdvaOLD
282. raleqf
283. rexeqf
284. rexeqfOLD
285. raleqbid
286. rexeqbid
287. sbralie
288. sbralieALT
289. cbvralf
290. cbvrexf
291. cbvral
292. cbvrex
293. cbvralv
294. cbvrexv
295. cbvralsv
296. cbvrexsv
297. cbvral2v
298. cbvrex2v
299. cbvral3v
300. rgen2a
301. nfrald
302. nfrexd
303. nfral
304. nfrex
305. nfra2
306. 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. cbvreuwOLD
39. rmoeq1
40. reueq1
41. rmoeq1OLD
42. reueq1OLD
43. rmoeqd
44. reueqd
45. reueqdv
46. reueqbidv
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. rabeqbidvaOLD
20. rabeqbidv
21. rabrabi
22. nfrab1
23. rabid
24. rabidim1
25. reqabi
26. rabrab
27. rabbida4
28. rabbida
29. rabbid
30. rabeqd
31. rabeqbida
32. rabbi
33. rabid2f
34. rabid2im
35. rabid2
36. rabid2OLD
37. rabeqf
38. cbvrabw
39. cbvrabwOLD
40. nfrabw
41. nfrabwOLD
42. rabbidaOLD
43. nfrab
44. cbvrab