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