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