Metamath Proof Explorer

Table of Contents - 2.3. ZF Set Theory - add the Axiom of Power Sets

Introduce the Axiom of Power Sets
1. ax-pow
2. zfpow
3. axpow2
4. axpow3
5. elALT2
6. dtruALT2
7. dtrucor
8. dtrucor2
9. dvdemo1
10. dvdemo2
11. nfnid
12. nfcvb
13. vpwex
14. pwexg
15. pwexd
16. pwex
17. pwel
18. abssexg
19. snexALT
20. p0ex
21. p0exALT
22. pp0ex
23. ord3ex
24. dtruALT
25. axc16b
26. eunex
27. eusv1
28. eusvnf
29. eusvnfb
30. eusv2i
31. eusv2nf
32. eusv2
33. reusv1
34. reusv2lem1
35. reusv2lem2
36. reusv2lem3
37. reusv2lem4
38. reusv2lem5
39. reusv2
40. reusv3i
41. reusv3
42. eusv4
43. alxfr
44. ralxfrd
45. rexxfrd
46. ralxfr2d
47. rexxfr2d
48. ralxfrd2
49. rexxfrd2
50. ralxfr
51. ralxfrALT
52. rexxfr
53. rabxfrd
54. rabxfr
55. reuhypd
56. reuhyp
57. zfpair
58. axprALT
Derive the Axiom of Pairing
1. axprlem1
2. axprlem2
3. axprlem3
4. axprlem4
5. axprlem5
6. axpr
7. ax-pr
8. zfpair2
9. snex
10. prex
11. sels
12. el
13. elALT
14. dtru
15. snelpwi
16. snelpw
17. prelpw
18. prelpwi
19. rext
20. sspwb
21. unipw
22. univ
23. pwtr
24. ssextss
25. ssext
26. nssss
27. pweqb
28. intid
29. moabex
30. rmorabex
31. euabex
32. nnullss
33. exss
34. opex
35. otex
36. elopg
37. elop
38. opi1
39. opi2
40. opeluu
41. op1stb
42. brv
Ordered pair theorem
1. opnz
2. opnzi
3. opth1
4. opth
5. opthg
6. opth1g
7. opthg2
8. opth2
9. opthneg
10. opthne
11. otth2
12. otth
13. otthg
14. eqvinop
15. sbcop1
16. sbcop
17. copsexgw
18. copsexg
19. copsex2t
20. copsex2g
21. copsex2gOLD
22. copsex4g
23. 0nelop
24. opwo0id
25. opeqex
26. oteqex2
27. oteqex
28. opcom
29. moop2
30. opeqsng
31. opeqsn
32. opeqpr
33. snopeqop
34. propeqop
35. propssopi
36. snopeqopsnid
37. mosubopt
38. mosubop
39. euop2
40. euotd
41. opthwiener
42. uniop
43. uniopel
44. opthhausdorff
45. opthhausdorff0
46. otsndisj
47. otiunsndisj
48. iunopeqop
49. brsnop
Ordered-pair class abstractions (cont.)
1. opabidw
2. opabid
3. elopab
4. rexopabb
5. vopelopabsb
6. opelopabsb
7. brabsb
8. opelopabt
9. opelopabga
10. brabga
11. opelopab2a
12. opelopaba
13. braba
14. opelopabg
15. brabg
16. opelopabgf
17. opelopab2
18. opelopab
19. brab
20. opelopabaf
21. opelopabf
22. ssopab2
23. ssopab2bw
24. eqopab2bw
25. ssopab2b
26. ssopab2i
27. ssopab2dv
28. eqopab2b
29. opabn0
30. opab0
31. csbopab
32. csbopabgALT
33. csbmpt12
34. csbmpt2
35. iunopab
36. elopabr
37. elopabran
38. rbropapd
39. rbropap
40. 2rbropap
41. 0nelopab
42. 0nelopabOLD
43. brabv
Power class of union and intersection
1. pwin
2. pwunssOLD
3. pwssun
4. pwundifOLD
5. pwun
The identity relation
1. cid
2. df-id
3. dfid4
4. dfid2
5. dfid3
6. dfid2OLD
The membership relation (or epsilon relation)
1. cep
2. df-eprel
3. epelg
4. epeli
5. epel
6. 0sn0ep
7. epn0
Partial and total orderings
1. wpo
2. wor
3. df-po
4. df-so
5. poss
6. poeq1
7. poeq2
8. nfpo
9. nfso
10. pocl
11. poclOLD
12. ispod
13. swopolem
14. swopo
15. poirr
16. potr
17. po2nr
18. po3nr
19. po2ne
20. po0
21. pofun
22. sopo
23. soss
24. soeq1
25. soeq2
26. sonr
27. sotr
28. solin
29. so2nr
30. so3nr
31. sotric
32. sotrieq
33. sotrieq2
34. soasym
35. sotr2
36. issod
37. issoi
38. isso2i
39. so0
40. somo
Founded and well-ordering relations
1. wfr
2. wse
3. wwe
4. df-fr
5. df-se
6. df-we
7. dffr6
8. frd
9. fri
10. friOLD
11. seex
12. exse
13. dffr2
14. dffr2ALT
15. frc
16. frss
17. sess1
18. sess2
19. freq1
20. freq2
21. seeq1
22. seeq2
23. nffr
24. nfse
25. nfwe
26. frirr
27. fr2nr
28. fr0
29. frminex
30. efrirr
31. efrn2lp
32. epse
33. tz7.2
34. dfepfr
35. epfrc
36. wess
37. weeq1
38. weeq2
39. wefr
40. weso
41. wecmpep
42. wetrep
43. wefrc
44. we0
45. wereu
46. wereu2
Relations
1. cxp
2. ccnv
3. cdm
4. crn
5. cres
6. cima
7. ccom
8. wrel
9. df-xp
10. df-rel
11. df-cnv
12. df-co
13. df-dm
14. df-rn
15. df-res
16. df-ima
17. xpeq1
18. xpss12
19. xpss
20. inxpssres
21. relxp
22. xpss1
23. xpss2
24. xpeq2
25. elxpi
26. elxp
27. elxp2
28. xpeq12
29. xpeq1i
30. xpeq2i
31. xpeq12i
32. xpeq1d
33. xpeq2d
34. xpeq12d
35. sqxpeqd
36. nfxp
37. 0nelxp
38. 0nelelxp
39. opelxp
40. opelxpi
41. opelxpd
42. opelvv
43. opelvvg
44. opelxp1
45. opelxp2
46. otelxp1
47. otel3xp
48. opabssxpd
49. rabxp
50. brxp
51. pwvrel
52. pwvabrel
53. brrelex12
54. brrelex1
55. brrelex2
56. brrelex12i
57. brrelex1i
58. brrelex2i
59. nprrel12
60. nprrel
61. 0nelrel0
62. 0nelrel
63. fconstmpt
64. vtoclr
65. opthprc
66. brel
67. elxp3
68. opeliunxp
69. xpundi
70. xpundir
71. xpiundi
72. xpiundir
73. iunxpconst
74. xpun
75. elvv
76. elvvv
77. elvvuni
78. brinxp2
79. brinxp
80. opelinxp
81. poinxp
82. soinxp
83. frinxp
84. seinxp
85. weinxp
86. posn
87. sosn
88. frsn
89. wesn
90. elopaelxp
91. bropaex12
92. opabssxp
93. brab2a
94. optocl
95. 2optocl
96. 3optocl
97. opbrop
98. 0xp
99. csbxp
100. releq
101. releqi
102. releqd
103. nfrel
104. sbcrel
105. relss
106. ssrel
107. eqrel
108. ssrel2
109. relssi
110. relssdv
111. eqrelriv
112. eqrelriiv
113. eqbrriv
114. eqrelrdv
115. eqbrrdv
116. eqbrrdiv
117. eqrelrdv2
118. ssrelrel
119. eqrelrel
120. elrel
121. rel0
122. nrelv
123. relsng
124. relsnb
125. relsnopg
126. relsn
127. relsnop
128. copsex2gb
129. copsex2ga
130. elopaba
131. xpsspw
132. unixpss
133. relun
134. relin1
135. relin2
136. relinxp
137. reldif
138. reliun
139. reliin
140. reluni
141. relint
142. relopabiv
143. relopabv
144. relopabi
145. relopabiALT
146. relopab
147. mptrel
148. reli
149. rele
150. opabid2
151. inopab
152. difopab
153. inxp
154. xpindi
155. xpindir
156. xpiindi
157. xpriindi
158. eliunxp
159. opeliunxp2
160. raliunxp
161. rexiunxp
162. ralxp
163. rexxp
164. exopxfr
165. exopxfr2
166. djussxp
167. ralxpf
168. rexxpf
169. iunxpf
170. opabbi2dv
171. relop
172. ideqg
173. ideq
174. ididg
175. issetid
176. coss1
177. coss2
178. coeq1
179. coeq2
180. coeq1i
181. coeq2i
182. coeq1d
183. coeq2d
184. coeq12i
185. coeq12d
186. nfco
187. brcog
188. opelco2g
189. brcogw
190. eqbrrdva
191. brco
192. opelco
193. cnvss
194. cnveq
195. cnveqi
196. cnveqd
197. elcnv
198. elcnv2
199. nfcnv
200. brcnvg
201. opelcnvg
202. opelcnv
203. brcnv
204. csbcnv
205. csbcnvgALT
206. cnvco
207. cnvuni
208. dfdm3
209. dfrn2
210. dfrn3
211. elrn2g
212. elrng
213. elrn2
214. elrn
215. ssrelrn
216. dfdm4
217. dfdmf
218. csbdm
219. eldmg
220. eldm2g
221. eldm
222. eldm2
223. dmss
224. dmeq
225. dmeqi
226. dmeqd
227. opeldmd
228. opeldm
229. breldm
230. breldmg
231. dmun
232. dmin
233. breldmd
234. dmiun
235. dmuni
236. dmopab
237. dmopabelb
238. dmopab2rex
239. dmopabss
240. dmopab3
241. dm0
242. dmi
243. dmv
244. dmep
245. domepOLD
246. dm0rn0
247. rn0
248. rnep
249. reldm0
250. dmxp
251. dmxpid
252. dmxpin
253. xpid11
254. dmcnvcnv
255. rncnvcnv
256. elreldm
257. rneq
258. rneqi
259. rneqd
260. rnss
261. rnssi
262. brelrng
263. brelrn
264. opelrn
265. releldm
266. relelrn
267. releldmb
268. relelrnb
269. releldmi
270. relelrni
271. dfrnf
272. nfdm
273. nfrn
274. dmiin
275. rnopab
276. rnmpt
277. elrnmpt
278. elrnmpt1s
279. elrnmpt1
280. elrnmptg
281. elrnmpti
282. elrnmptd
283. elrnmptdv
284. elrnmpt2d
285. dfiun3g
286. dfiin3g
287. dfiun3
288. dfiin3
289. riinint
290. relrn0
291. dmrnssfld
292. dmcoss
293. rncoss
294. dmcosseq
295. dmcoeq
296. rncoeq
297. reseq1
298. reseq2
299. reseq1i
300. reseq2i
301. reseq12i
302. reseq1d
303. reseq2d
304. reseq12d
305. nfres
306. csbres
307. res0
308. dfres3
309. opelres
310. brres
311. opelresi
312. brresi
313. opres
314. resieq
315. opelidres
316. resres
317. resundi
318. resundir
319. resindi
320. resindir
321. inres
322. resdifcom
323. resiun1
324. resiun2
325. dmres
326. ssdmres
327. dmresexg
328. resss
329. rescom
330. ssres
331. ssres2
332. relres
333. resabs1
334. resabs1d
335. resabs2
336. residm
337. resima
338. resima2
339. rnresss
340. xpssres
341. elinxp
342. elres
343. elsnres
344. relssres
345. dmressnsn
346. eldmressnsn
347. eldmeldmressn
348. resdm
349. resexg
350. resexd
351. resex
352. resindm
353. resdmdfsn
354. resopab
355. iss
356. resopab2
357. resmpt
358. resmpt3
359. resmptf
360. resmptd
361. dfres2
362. mptss
363. elidinxp
364. elidinxpid
365. elrid
366. idinxpres
367. idinxpresid
368. idssxp
369. opabresid
370. mptresid
371. opabresidOLD
372. mptresidOLD
373. dmresi
374. restidsing
375. iresn0n0
376. imaeq1
377. imaeq2
378. imaeq1i
379. imaeq2i
380. imaeq1d
381. imaeq2d
382. imaeq12d
383. dfima2
384. dfima3
385. elimag
386. elima
387. elima2
388. elima3
389. nfima
390. nfimad
391. imadmrn
392. imassrn
393. mptima
394. imai
395. rnresi
396. resiima
397. ima0
398. 0ima
399. csbima12
400. imadisj
401. cnvimass
402. cnvimarndm
403. imasng
404. relimasn
405. elrelimasn
406. elimasng1
407. elimasn1
408. elimasng
409. elimasn
410. elimasngOLD
411. elimasni
412. args
413. elinisegg
414. eliniseg
415. epin
416. epini
417. iniseg
418. inisegn0
419. dffr3
420. dfse2
421. imass1
422. imass2
423. ndmima
424. relcnv
425. relbrcnvg
426. eliniseg2
427. relbrcnv
428. cotrg
429. cotr
430. idrefALT
431. cnvsym
432. intasym
433. asymref
434. asymref2
435. intirr
436. brcodir
437. codir
438. qfto
439. xpidtr
440. trin2
441. poirr2
442. trinxp
443. soirri
444. sotri
445. son2lpi
446. sotri2
447. sotri3
448. poleloe
449. poltletr
450. somin1
451. somincom
452. somin2
453. soltmin
454. cnvopab
455. mptcnv
456. cnv0
457. cnvi
458. cnvun
459. cnvdif
460. cnvin
461. rnun
462. rnin
463. rniun
464. rnuni
465. imaundi
466. imaundir
467. cnvimassrndm
468. dminss
469. imainss
470. inimass
471. inimasn
472. cnvxp
473. xp0
474. xpnz
475. xpeq0
476. xpdisj1
477. xpdisj2
478. xpsndisj
479. difxp
480. difxp1
481. difxp2
482. djudisj
483. xpdifid
484. resdisj
485. rnxp
486. dmxpss
487. rnxpss
488. rnxpid
489. ssxpb
490. xp11
491. xpcan
492. xpcan2
493. ssrnres
494. rninxp
495. dminxp
496. imainrect
497. xpima
498. xpima1
499. xpima2
500. xpimasn
501. sossfld
502. sofld
503. cnvcnv3
504. dfrel2
505. dfrel4v
506. dfrel4
507. cnvcnv
508. cnvcnv2
509. cnvcnvss
510. cnvrescnv
511. cnveqb
512. cnveq0
513. dfrel3
514. elid
515. dmresv
516. rnresv
517. dfrn4
518. csbrn
519. rescnvcnv
520. cnvcnvres
521. imacnvcnv
522. dmsnn0
523. rnsnn0
524. dmsn0
525. cnvsn0
526. dmsn0el
527. relsn2
528. dmsnopg
529. dmsnopss
530. dmpropg
531. dmsnop
532. dmprop
533. dmtpop
534. cnvcnvsn
535. dmsnsnsn
536. rnsnopg
537. rnpropg
538. cnvsng
539. rnsnop
540. op1sta
541. cnvsn
542. op2ndb
543. op2nda
544. opswap
545. cnvresima
546. resdm2
547. resdmres
548. resresdm
549. imadmres
550. resdmss
551. resdifdi
552. resdifdir
553. mptpreima
554. mptiniseg
555. dmmpt
556. dmmptss
557. dmmptg
558. rnmpt0f
559. rnmptn0
560. relco
561. dfco2
562. dfco2a
563. coundi
564. coundir
565. cores
566. resco
567. imaco
568. rnco
569. rnco2
570. dmco
571. coeq0
572. coiun
573. cocnvcnv1
574. cocnvcnv2
575. cores2
576. co02
577. co01
578. coi1
579. coi2
580. coires1
581. coass
582. relcnvtrg
583. relcnvtr
584. relssdmrn
585. resssxp
586. cnvssrndm
587. cossxp
588. relrelss
589. unielrel
590. relfld
591. relresfld
592. relcoi2
593. relcoi1
594. unidmrn
595. relcnvfld
596. dfdm2
597. unixp
598. unixp0
599. unixpid
600. ressn
601. cnviin
602. cnvpo
603. cnvso
604. xpco
605. xpcoid
606. elsnxp
607. reu3op
608. reuop
609. opreu2reurex
610. opreu2reu
611. dfpo2
612. csbcog
The Predecessor Class
1. cpred
2. df-pred
3. predeq123
4. predeq1
5. predeq2
6. predeq3
7. nfpred
8. csbpredg
9. predpredss
10. predss
11. sspred
12. dfpred2
13. dfpred3
14. dfpred3g
15. elpredgg
16. elpredg
17. elpredimg
18. elpredim
19. elpred
20. predexg
21. predasetexOLD
22. dffr4
23. predel
24. predbrg
25. predtrss
26. predpo
27. predso
28. setlikespec
29. predidm
30. predin
31. predun
32. preddif
33. predep
34. trpred
35. preddowncl
36. predpoirr
37. predfrirr
38. pred0
39. dfse3
40. predrelss
41. predprc
42. predres
Well-founded induction (variant)
1. frpomin
2. frpomin2
3. frpoind
4. frpoinsg
5. frpoins2fg
6. frpoins2g
7. frpoins3g
Well-ordered induction
1. tz6.26
2. tz6.26OLD
3. tz6.26i
4. wfi
5. wfiOLD
6. wfii
7. wfisg
8. wfisgOLD
9. wfis
10. wfis2fg
11. wfis2fgOLD
12. wfis2f
13. wfis2g
14. wfis2
15. wfis3
Ordinals
1. word
2. con0
3. wlim
4. csuc
5. df-ord
6. df-on
7. df-lim
8. df-suc
9. ordeq
10. elong
11. elon
12. eloni
13. elon2
14. limeq
15. ordwe
16. ordtr
17. ordfr
18. ordelss
19. trssord
20. ordirr
21. nordeq
22. ordn2lp
23. tz7.5
24. ordelord
25. tron
26. ordelon
27. onelon
28. tz7.7
29. ordelssne
30. ordelpss
31. ordsseleq
32. ordin
33. onin
34. ordtri3or
35. ordtri1
36. ontri1
37. ordtri2
38. ordtri3
39. ordtri4
40. orddisj
41. onfr
42. onelpss
43. onsseleq
44. onelss
45. ordtr1
46. ordtr2
47. ordtr3
48. ontr1
49. ontr2
50. ordunidif
51. ordintdif
52. onintss
53. oneqmini
54. ord0
55. 0elon
56. ord0eln0
57. on0eln0
58. dflim2
59. inton
60. nlim0
61. limord
62. limuni
63. limuni2
64. 0ellim
65. limelon
66. onn0
67. suceq
68. elsuci
69. elsucg
70. elsuc2g
71. elsuc
72. elsuc2
73. nfsuc
74. elelsuc
75. sucel
76. suc0
77. sucprc
78. unisuc
79. sssucid
80. sucidg
81. sucid
82. nsuceq0
83. eqelsuc
84. iunsuc
85. suctr
86. trsuc
87. trsucss
88. ordsssuc
89. onsssuc
90. ordsssuc2
91. onmindif
92. ordnbtwn
93. onnbtwn
94. sucssel
95. orddif
96. orduniss
97. ordtri2or
98. ordtri2or2
99. ordtri2or3
100. ordelinel
101. ordssun
102. ordequn
103. ordun
104. ordunisssuc
105. suc11
106. onun2
107. onordi
108. ontrci
109. onirri
110. oneli
111. onelssi
112. onssneli
113. onssnel2i
114. onelini
115. oneluni
116. onunisuci
117. onsseli
118. onun2i
119. unizlim
120. on0eqel
121. snsn0non
122. onxpdisj
123. onnev
124. onnevOLD
Definite description binder (inverted iota)
1. cio
2. iotajust
3. df-iota
4. dfiota2
5. nfiota1
6. nfiotadw
7. nfiotaw
8. nfiotad
9. nfiota
10. cbviotaw
11. cbviotavw
12. cbviotavwOLD
13. cbviota
14. cbviotav
15. sb8iota
16. iotaeq
17. iotabi
18. uniabio
19. iotaval
20. iotauni
21. iotaint
22. iota1
23. iotanul
24. iotassuni
25. iotaex
26. iota4
27. iota4an
28. iota5
29. iotabidv
30. iotabii
31. iotacl
32. iota2df
33. iota2d
34. iota2
35. iotan0
36. sniota
37. dfiota4
38. csbiota
Functions
1. wfun
2. wfn
3. wf
4. wf1
5. wfo
6. wf1o
7. cfv
8. wiso
9. df-fun
10. df-fn
11. df-f
12. df-f1
13. df-fo
14. df-f1o
15. df-fv
16. df-isom
17. dffun2
18. dffun3
19. dffun4
20. dffun5
21. dffun6f
22. dffun6
23. funmo
24. funrel
25. 0nelfun
26. funss
27. funeq
28. funeqi
29. funeqd
30. nffun
31. sbcfung
32. funeu
33. funeu2
34. dffun7
35. dffun8
36. dffun9
37. funfn
38. funfnd
39. funi
40. nfunv
41. funopg
42. funopab
43. funopabeq
44. funopab4
45. funmpt
46. funmpt2
47. funco
48. funresfunco
49. funres
50. funresd
51. funssres
52. fun2ssres
53. funun
54. fununmo
55. fununfun
56. fundif
57. funcnvsn
58. funsng
59. fnsng
60. funsn
61. funprg
62. funtpg
63. funpr
64. funtp
65. fnsn
66. fnprg
67. fntpg
68. fntp
69. funcnvpr
70. funcnvtp
71. funcnvqp
72. fun0
73. funcnv0
74. funcnvcnv
75. funcnv2
76. funcnv
77. funcnv3
78. fun2cnv
79. svrelfun
80. fncnv
81. fun11
82. fununi
83. funin
84. funres11
85. funcnvres
86. cnvresid
87. funcnvres2
88. funimacnv
89. funimass1
90. funimass2
91. imadif
92. imain
93. funimaexg
94. funimaex
95. isarep1
96. isarep2
97. fneq1
98. fneq2
99. fneq1d
100. fneq2d
101. fneq12d
102. fneq12
103. fneq1i
104. fneq2i
105. nffn
106. fnfun
107. fnfund
108. fnrel
109. fndm
110. fndmi
111. fndmd
112. funfni
113. fndmu
114. fnbr
115. fnop
116. fneu
117. fneu2
118. fnun
119. fnund
120. fnunop
121. fncofn
122. fnco
123. fncoOLD
124. fnresdm
125. fnresdisj
126. 2elresin
127. fnssresb
128. fnssres
129. fnssresd
130. fnresin1
131. fnresin2
132. fnres
133. idfn
134. fnresi
135. fnresiOLD
136. fnima
137. fn0
138. fnimadisj
139. fnimaeq0
140. dfmpt3
141. mptfnf
142. fnmptf
143. fnopabg
144. fnopab
145. mptfng
146. fnmpt
147. fnmptd
148. mpt0
149. fnmpti
150. dmmpti
151. dmmptd
152. mptun
153. partfun
154. feq1
155. feq2
156. feq3
157. feq23
158. feq1d
159. feq2d
160. feq3d
161. feq12d
162. feq123d
163. feq123
164. feq1i
165. feq2i
166. feq12i
167. feq23i
168. feq23d
169. nff
170. sbcfng
171. sbcfg
172. elimf
173. ffn
174. ffnd
175. dffn2
176. ffun
177. ffund
178. frel
179. freld
180. frn
181. frnd
182. fdm
183. fdmOLD
184. fdmd
185. fdmi
186. dffn3
187. ffrn
188. ffrnb
189. ffrnbd
190. fss
191. fssd
192. fssdmd
193. fssdm
194. fimass
195. fimacnv
196. fcof
197. fco
198. fcoOLD
199. fcod
200. fco2
201. fssxp
202. funssxp
203. ffdm
204. ffdmd
205. fdmrn
206. funcofd
207. fco3OLD
208. opelf
209. fun
210. fun2
211. fun2d
212. fnfco
213. fssres
214. fssresd
215. fssres2
216. fresin
217. resasplit
218. fresaun
219. fresaunres2
220. fresaunres1
221. fcoi1
222. fcoi2
223. feu
224. fcnvres
225. fimacnvdisj
226. fint
227. fin
228. f0
229. f00
230. f0bi
231. f0dom0
232. f0rn0
233. fconst
234. fconstg
235. fnconstg
236. fconst6g
237. fconst6
238. f1eq1
239. f1eq2
240. f1eq3
241. nff1
242. dff12
243. f1f
244. f1fn
245. f1fun
246. f1rel
247. f1dm
248. f1dmOLD
249. f1ss
250. f1ssr
251. f1ssres
252. f1resf1
253. f1cnvcnv
254. f1cof1
255. f1co
256. f1coOLD
257. foeq1
258. foeq2
259. foeq3
260. nffo
261. fof
262. fofun
263. fofn
264. forn
265. dffo2
266. foima
267. dffn4
268. funforn
269. fodmrnu
270. fimadmfo
271. fores
272. fimadmfoALT
273. focnvimacdmdm
274. focofo
275. foco
276. foconst
277. f1oeq1
278. f1oeq2
279. f1oeq3
280. f1oeq23
281. f1eq123d
282. foeq123d
283. f1oeq123d
284. f1oeq1d
285. f1oeq2d
286. f1oeq3d
287. nff1o
288. f1of1
289. f1of
290. f1ofn
291. f1ofun
292. f1orel
293. f1odm
294. dff1o2
295. dff1o3
296. f1ofo
297. dff1o4
298. dff1o5
299. f1orn
300. f1f1orn
301. f1ocnv
302. f1ocnvb
303. f1ores
304. f1orescnv
305. f1imacnv
306. foimacnv
307. foun
308. f1oun
309. resdif
310. resin
311. f1oco
312. f1cnv
313. funcocnv2
314. fococnv2
315. f1ococnv2
316. f1cocnv2
317. f1ococnv1
318. f1cocnv1
319. funcoeqres
320. f1ssf1
321. f10
322. f10d
323. f1o00
324. fo00
325. f1o0
326. f1oi
327. f1ovi
328. f1osn
329. f1osng
330. f1sng
331. fsnd
332. f1oprswap
333. f1oprg
334. tz6.12-2
335. fveu
336. brprcneu
337. brprcneuALT
338. fvprc
339. fvprcALT
340. rnfvprc
341. fv2
342. dffv3
343. dffv4
344. elfv
345. fveq1
346. fveq2
347. fveq1i
348. fveq1d
349. fveq2i
350. fveq2d
351. 2fveq3
352. fveq12i
353. fveq12d
354. fveqeq2d
355. fveqeq2
356. nffv
357. nffvmpt1
358. nffvd
359. fvex
360. fvexi
361. fvexd
362. fvif
363. iffv
364. fv3
365. fvres
366. fvresd
367. funssfv
368. tz6.12-1
369. tz6.12
370. tz6.12f
371. tz6.12c
372. tz6.12i
373. fvbr0
374. fvrn0
375. fvssunirn
376. ndmfv
377. ndmfvrcl
378. elfvdm
379. elfvex
380. elfvexd
381. eliman0
382. nfvres
383. nfunsn
384. fvfundmfvn0
385. 0fv
386. fv2prc
387. elfv2ex
388. fveqres
389. csbfv12
390. csbfv2g
391. csbfv
392. funbrfv
393. funopfv
394. fnbrfvb
395. fnopfvb
396. funbrfvb
397. funopfvb
398. fnbrfvb2
399. funbrfv2b
400. dffn5
401. fnrnfv
402. fvelrnb
403. foelrni
404. dfimafn
405. dfimafn2
406. funimass4
407. fvelima
408. fvelimad
409. feqmptd
410. feqresmpt
411. feqmptdf
412. dffn5f
413. fvelimab
414. fvelimabd
415. unima
416. fvi
417. fviss
418. fniinfv
419. fnsnfv
420. fnsnfvOLD
421. opabiotafun
422. opabiotadm
423. opabiota
424. fnimapr
425. ssimaex
426. ssimaexg
427. funfv
428. funfv2
429. funfv2f
430. fvun
431. fvun1
432. fvun2
433. fvun1d
434. fvun2d
435. dffv2
436. dmfco
437. fvco2
438. fvco
439. fvco3
440. fvco3d
441. fvco4i
442. fvopab3g
443. fvopab3ig
444. brfvopabrbr
445. fvmptg
446. fvmpti
447. fvmpt
448. fvmpt2f
449. fvtresfn
450. fvmpts
451. fvmpt3
452. fvmpt3i
453. fvmptdf
454. fvmptd
455. fvmptd2
456. mptrcl
457. fvmpt2i
458. fvmpt2
459. fvmptss
460. fvmpt2d
461. fvmptex
462. fvmptd3f
463. fvmptd2f
464. fvmptdv
465. fvmptdv2
466. mpteqb
467. fvmptt
468. fvmptf
469. fvmptnf
470. fvmptd3
471. fvmptn
472. fvmptss2
473. elfvmptrab1w
474. elfvmptrab1
475. elfvmptrab
476. fvopab4ndm
477. fvmptndm
478. fvmptrabfv
479. fvopab5
480. fvopab6
481. eqfnfv
482. eqfnfv2
483. eqfnfv3
484. eqfnfvd
485. eqfnfv2f
486. eqfunfv
487. fvreseq0
488. fvreseq1
489. fvreseq
490. fnmptfvd
491. fndmdif
492. fndmdifcom
493. fndmdifeq0
494. fndmin
495. fneqeql
496. fneqeql2
497. fnreseql
498. chfnrn
499. funfvop
500. funfvbrb
501. fvimacnvi
502. fvimacnv
503. funimass3
504. funimass5
505. funconstss
506. fvimacnvALT
507. elpreima
508. elpreimad
509. fniniseg
510. fncnvima2
511. fniniseg2
512. unpreima
513. inpreima
514. difpreima
515. respreima
516. cnvimainrn
517. sspreima
518. iinpreima
519. intpreima
520. fimacnvOLD
521. fimacnvinrn
522. fimacnvinrn2
523. rescnvimafod
524. fvn0ssdmfun
525. fnopfv
526. fvelrn
527. nelrnfvne
528. fveqdmss
529. fveqressseq
530. fnfvelrn
531. ffvelrn
532. ffvelrni
533. ffvelrnda
534. ffvelrnd
535. rexrn
536. ralrn
537. elrnrexdm
538. elrnrexdmb
539. eldmrexrn
540. eldmrexrnb
541. fvcofneq
542. ralrnmptw
543. rexrnmptw
544. ralrnmpt
545. rexrnmpt
546. f0cli
547. dff2
548. dff3
549. dff4
550. dffo3
551. dffo4
552. dffo5
553. exfo
554. foelrn
555. foco2
556. fmpt
557. f1ompt
558. fmpti
559. fvmptelrn
560. fmptd
561. fmpttd
562. fmpt3d
563. fmptdf
564. ffnfv
565. ffnfvf
566. fnfvrnss
567. frnssb
568. rnmptss
569. fmpt2d
570. ffvresb
571. f1oresrab
572. f1ossf1o
573. fmptco
574. fmptcof
575. fmptcos
576. cofmpt
577. fcompt
578. fcoconst
579. fsn
580. fsn2
581. fsng
582. fsn2g
583. xpsng
584. xpprsng
585. xpsn
586. f1o2sn
587. residpr
588. dfmpt
589. fnasrn
590. idref
591. funiun
592. funopsn
593. funop
594. funopdmsn
595. funsndifnop
596. funsneqopb
597. ressnop0
598. fpr
599. fprg
600. ftpg
601. ftp
602. fnressn
603. funressn
604. fressnfv
605. fvrnressn
606. fvressn
607. fvn0fvelrn
608. fvconst
609. fnsnr
610. fnsnb
611. fmptsn
612. fmptsng
613. fmptsnd
614. fmptap
615. fmptapd
616. fmptpr
617. fvresi
618. fninfp
619. fnelfp
620. fndifnfp
621. fnelnfp
622. fnnfpeq0
623. fvunsn
624. fvsng
625. fvsn
626. fvsnun1
627. fvsnun2
628. fnsnsplit
629. fsnunf
630. fsnunf2
631. fsnunfv
632. fsnunres
633. funresdfunsn
634. fvpr1g
635. fvpr2g
636. fvpr2gOLD
637. fvpr1
638. fvpr1OLD
639. fvpr2
640. fvpr2OLD
641. fprb
642. fvtp1
643. fvtp2
644. fvtp3
645. fvtp1g
646. fvtp2g
647. fvtp3g
648. tpres
649. fvconst2g
650. fconst2g
651. fvconst2
652. fconst2
653. fconst5
654. rnmptc
655. rnmptcOLD
656. fnprb
657. fntpb
658. fnpr2g
659. fpr2g
660. fconstfv
661. fconst3
662. fconst4
663. resfunexg
664. resiexd
665. fnex
666. fnexd
667. funex
668. opabex
669. mptexg
670. mptexgf
671. mptex
672. mptexd
673. mptrabex
674. fex
675. fexd
676. mptfvmpt
677. eufnfv
678. funfvima
679. funfvima2
680. funfvima2d
681. fnfvima
682. fnfvimad
683. resfvresima
684. funfvima3
685. rexima
686. ralima
687. fvclss
688. elabrex
689. abrexco
690. imaiun
691. imauni
692. fniunfv
693. funiunfv
694. funiunfvf
695. eluniima
696. elunirn
697. elunirnALT
698. elunirn2
699. fnunirn
700. dff13
701. dff13f
702. f1veqaeq
703. f1cofveqaeq
704. f1cofveqaeqALT
705. 2f1fvneq
706. f1mpt
707. f1fveq
708. f1elima
709. f1imass
710. f1imaeq
711. f1imapss
712. fpropnf1
713. f1dom3fv3dif
714. f1dom3el3dif
715. dff14a
716. dff14b
717. f12dfv
718. f13dfv
719. dff1o6
720. f1ocnvfv1
721. f1ocnvfv2
722. f1ocnvfv
723. f1ocnvfvb
724. nvof1o
725. nvocnv
726. fsnex
727. f1prex
728. f1ocnvdm
729. f1ocnvfvrneq
730. fcof1
731. fcofo
732. cbvfo
733. cbvexfo
734. cocan1
735. cocan2
736. fcof1oinvd
737. fcof1od
738. 2fcoidinvd
739. fcof1o
740. 2fvcoidd
741. 2fvidf1od
742. 2fvidinvd
743. foeqcnvco
744. f1eqcocnv
745. f1eqcocnvOLD
746. fveqf1o
747. nf1const
748. nf1oconst
749. f1ofvswap
750. fliftrel
751. fliftel
752. fliftel1
753. fliftcnv
754. fliftfun
755. fliftfund
756. fliftfuns
757. fliftf
758. fliftval
759. isoeq1
760. isoeq2
761. isoeq3
762. isoeq4
763. isoeq5
764. nfiso
765. isof1o
766. isof1oidb
767. isof1oopb
768. isorel
769. soisores
770. soisoi
771. isoid
772. isocnv
773. isocnv2
774. isocnv3
775. isores2
776. isores1
777. isores3
778. isotr
779. isomin
780. isoini
781. isoini2
782. isofrlem
783. isoselem
784. isofr
785. isose
786. isofr2
787. isopolem
788. isopo
789. isosolem
790. isoso
791. isowe
792. isowe2
793. f1oiso
794. f1oiso2
795. f1owe
796. weniso
797. weisoeq
798. weisoeq2
799. knatar
Cantor's Theorem
1. canth
2. ncanth
Restricted iota (description binder)
1. crio
2. df-riota
3. riotaeqdv
4. riotabidv
5. riotaeqbidv
6. riotaex
7. riotav
8. riotauni
9. nfriota1
10. nfriotadw
11. cbvriotaw
12. cbvriotavw
13. cbvriotavwOLD
14. nfriotad
15. nfriota
16. cbvriota
17. cbvriotav
18. csbriota
19. riotacl2
20. riotacl
21. riotasbc
22. riotabidva
23. riotabiia
24. riota1
25. riota1a
26. riota2df
27. riota2f
28. riota2
29. riotaeqimp
30. riotaprop
31. riota5f
32. riota5
33. riotass2
34. riotass
35. moriotass
36. snriota
37. riotaxfrd
38. eusvobj2
39. eusvobj1
40. f1ofveu
41. f1ocnvfv3
42. riotaund
43. riotassuni
44. riotaclb
Operations
1. co
2. coprab
3. cmpo
4. df-ov
5. df-oprab
6. df-mpo
7. oveq
8. oveq1
9. oveq2
10. oveq12
11. oveq1i
12. oveq2i
13. oveq12i
14. oveqi
15. oveq123i
16. oveq1d
17. oveq2d
18. oveqd
19. oveq12d
20. oveqan12d
21. oveqan12rd
22. oveq123d
23. fvoveq1d
24. fvoveq1
25. ovanraleqv
26. imbrov2fvoveq
27. ovrspc2v
28. oveqrspc2v
29. oveqdr
30. nfovd
31. nfov
32. oprabidw
33. oprabid
34. ovex
35. ovexi
36. ovexd
37. ovssunirn
38. 0ov
39. ovprc
40. ovprc1
41. ovprc2
42. ovrcl
43. csbov123
44. csbov
45. csbov12g
46. csbov1g
47. csbov2g
48. rspceov
49. elovimad
50. fnbrovb
51. fnotovb
52. opabbrex
53. opabresex2d
54. fvmptopab
55. f1opr
56. brfvopab
57. dfoprab2
58. reloprab
59. oprabv
60. nfoprab1
61. nfoprab2
62. nfoprab3
63. nfoprab
64. oprabbid
65. oprabbidv
66. oprabbii
67. ssoprab2
68. ssoprab2b
69. eqoprab2bw
70. eqoprab2b
71. mpoeq123
72. mpoeq12
73. mpoeq123dva
74. mpoeq123dv
75. mpoeq123i
76. mpoeq3dva
77. mpoeq3ia
78. mpoeq3dv
79. nfmpo1
80. nfmpo2
81. nfmpo
82. 0mpo0
83. mpo0v
84. mpo0
85. oprab4
86. cbvoprab1
87. cbvoprab2
88. cbvoprab12
89. cbvoprab12v
90. cbvoprab3
91. cbvoprab3v
92. cbvmpox
93. cbvmpo
94. cbvmpov
95. elimdelov
96. ovif
97. ovif2
98. ovif12
99. ifov
100. dmoprab
101. dmoprabss
102. rnoprab
103. rnoprab2
104. reldmoprab
105. oprabss
106. eloprabga
107. eloprabgaOLD
108. eloprabg
109. ssoprab2i
110. mpov
111. mpomptx
112. mpompt
113. mpodifsnif
114. mposnif
115. fconstmpo
116. resoprab
117. resoprab2
118. resmpo
119. funoprabg
120. funoprab
121. fnoprabg
122. mpofun
123. mpofunOLD
124. fnoprab
125. ffnov
126. fovcl
127. eqfnov
128. eqfnov2
129. fnov
130. mpo2eqb
131. rnmpo
132. reldmmpo
133. elrnmpog
134. elrnmpo
135. elrnmpores
136. ralrnmpo
137. rexrnmpo
138. ovid
139. ovidig
140. ovidi
141. ov
142. ovigg
143. ovig
144. ovmpt4g
145. ovmpos
146. ov2gf
147. ovmpodxf
148. ovmpodx
149. ovmpod
150. ovmpox
151. ovmpoga
152. ovmpoa
153. ovmpodf
154. ovmpodv
155. ovmpodv2
156. ovmpog
157. ovmpo
158. fvmpopr2d
159. ov3
160. ov6g
161. ovg
162. ovres
163. ovresd
164. oprres
165. oprssov
166. fovrn
167. fovrnda
168. fovrnd
169. fnrnov
170. foov
171. fnovrn
172. ovelrn
173. funimassov
174. ovelimab
175. ovima0
176. ovconst2
177. oprssdm
178. nssdmovg
179. ndmovg
180. ndmov
181. ndmovcl
182. ndmovrcl
183. ndmovcom
184. ndmovass
185. ndmovdistr
186. ndmovord
187. ndmovordi
188. Variable-to-class conversion for operations
Maps-to notation
1. mpondm0
2. elmpocl
3. elmpocl1
4. elmpocl2
5. elovmpo
6. elovmporab
7. elovmporab1w
8. elovmporab1
9. 2mpo0
10. relmptopab
11. f1ocnvd
12. f1od
13. f1ocnv2d
14. f1o2d
15. f1opw2
16. f1opw
17. elovmpt3imp
18. ovmpt3rab1
19. ovmpt3rabdm
20. elovmpt3rab1
21. elovmpt3rab
Function operation
1. cof
2. cofr
3. df-of
4. df-ofr
5. ofeqd
6. ofeq
7. ofreq
8. ofexg
9. nfof
10. nfofr
11. ofrfvalg
12. offval
13. ofrfval
14. ofval
15. ofrval
16. offn
17. offun
18. offval2f
19. ofmresval
20. fnfvof
21. off
22. ofres
23. offval2
24. ofrfval2
25. ofmpteq
26. ofco
27. offveq
28. offveqb
29. ofc1
30. ofc2
31. ofc12
32. caofref
33. caofinvl
34. caofid0l
35. caofid0r
36. caofid1
37. caofid2
38. caofcom
39. caofrss
40. caofass
41. caoftrn
42. caofdi
43. caofdir
44. caonncan
Proper subset relation
1. crpss
2. df-rpss
3. relrpss
4. brrpssg
5. brrpss
6. porpss
7. sorpss
8. sorpssi
9. sorpssun
10. sorpssin
11. sorpssuni
12. sorpssint
13. sorpsscmpl