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. axpr
6. axprlem1OLD
7. axprlem3OLD
8. axprlem4OLD
9. axprlem5OLD
10. axprOLD
11. ax-pr
12. zfpair2
13. vsnex
14. axprglem
15. axprg
16. prex
17. snex
18. snexg
19. snexgALT
20. snexOLD
21. prexOLD
22. exel
23. exexneq
24. exneq
25. dtru
26. el
27. el.OLD
28. sels
29. selsALT
30. elALT
31. snelpwg
32. snelpwi
33. snelpw
34. prelpw
35. prelpwi
36. rext
37. sspwb
38. unipw
39. univ
40. pwtr
41. ssextss
42. ssext
43. nssss
44. pweqb
45. intidg
46. moabex
47. moabexOLD
48. rmorabex
49. euabex
50. nnullss
51. exss
52. opex
53. opexOLD
54. otex
55. elopg
56. elop
57. opi1
58. opi2
59. opeluu
60. op1stb
61. 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. otthne
15. eqvinop
16. sbcop1
17. sbcop
18. copsexgw
19. copsexgwOLD
20. copsexg
21. copsex2t
22. copsex2g
23. copsex2dv
24. copsex4g
25. 0nelop
26. opwo0id
27. opeqex
28. oteqex2
29. oteqex
30. opcom
31. moop2
32. opeqsng
33. opeqsn
34. opeqpr
35. snopeqop
36. propeqop
37. propssopi
38. snopeqopsnid
39. mosubopt
40. mosubop
41. euop2
42. euotd
43. opthwiener
44. uniop
45. uniopel
46. opthhausdorff
47. opthhausdorff0
48. otsndisj
49. otiunsndisj
50. iunopeqop
51. iunopeqopOLD
52. brsnop
53. brtp
Ordered-pair class abstractions (cont.)
1. opabidw
2. opabid
3. elopabw
4. elopab
5. rexopabb
6. vopelopabsb
7. opelopabsb
8. brabsb
9. opelopabt
10. opelopabga
11. brabga
12. opelopab2a
13. opelopaba
14. braba
15. brab2d
16. opelopabg
17. brabg
18. opelopabgf
19. opelopab2
20. opelopab
21. brab
22. opelopabaf
23. opelopabf
24. ssopab2
25. ssopab2bw
26. eqopab2bw
27. ssopab2b
28. ssopab2i
29. ssopab2dv
30. eqopab2b
31. opabn0
32. opab0
33. csbopab
34. csbopabw
35. csbmpt12
36. csbmpt2
37. iunopab
38. elopabr
39. elopabran
40. rbropapd
41. rbropap
42. 2rbropap
43. 0nelopab
44. brabv
Power class of union and intersection
1. pwin
2. pwssun
3. pwun
The identity relation
1. cid
2. df-id
3. dfid4
4. dfid2
5. dfid3
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. poeq12d
9. nfpo
10. nfso
11. pocl
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. soeq12d
27. sonr
28. sotr
29. sotrd
30. solin
31. so2nr
32. so3nr
33. sotric
34. sotrieq
35. sotrieq2
36. soasym
37. sotr2
38. issod
39. issoi
40. isso2i
41. so0
42. somo
43. sotrine
44. sotr3
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. seex
11. exse
12. dffr2
13. dffr2ALT
14. frc
15. frss
16. sess1
17. sess2
18. freq1
19. freq2
20. freq12d
21. seeq1
22. seeq2
23. seeq12d
24. nffr
25. nfse
26. nfwe
27. frirr
28. fr2nr
29. fr0
30. frminex
31. efrirr
32. efrn2lp
33. epse
34. tz7.2
35. dfepfr
36. epfrc
37. wess
38. weeq1
39. weeq2
40. weeq12d
41. wefr
42. weso
43. wecmpep
44. wetrep
45. wefrc
46. we0
47. wereu
48. 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. opelxpii
42. opelxpd
43. opelvv
44. opelvvg
45. opelxp1
46. opelxp2
47. otelxp
48. otelxp1
49. otel3xp
50. opabssxpd
51. rabxp
52. brxp
53. pwvrel
54. pwvabrel
55. brrelex12
56. brrelex1
57. brrelex2
58. brrelex12i
59. brrelex1i
60. brrelex2i
61. nprrel12
62. nprrel
63. 0nelrel0
64. 0nelrel
65. fconstmpt
66. vtoclr
67. opthprc
68. brel
69. elxp3
70. opeliunxp
71. opeliun2xp
72. xpundi
73. xpundir
74. xpiundi
75. xpiundir
76. iunxpconst
77. xpun
78. elvv
79. elvvv
80. elvvuni
81. brinxp2
82. brinxp
83. opelinxp
84. poinxp
85. soinxp
86. frinxp
87. seinxp
88. weinxp
89. posn
90. sosn
91. frsn
92. wesn
93. elopaelxp
94. bropaex12
95. opabssxp
96. brab2a
97. optocl
98. optoclOLD
99. 2optocl
100. 3optocl
101. opbrop
102. 0xp
103. xp0
104. csbxp
105. releq
106. releqi
107. releqd
108. nfrel
109. sbcrel
110. relss
111. ssrel
112. eqrel
113. ssrel2
114. ssrel3
115. relssi
116. relssdv
117. eqrelriv
118. eqrelriiv
119. eqbrriv
120. eqrelrdv
121. eqbrrdv
122. eqbrrdiv
123. eqrelrdv2
124. ssrelrel
125. eqrelrel
126. elrel
127. rel0
128. nrelv
129. nrelvOLD
130. relsng
131. relsnb
132. relsnopg
133. relsn
134. relsnop
135. copsex2gb
136. copsex2ga
137. elopaba
138. xpsspw
139. unixpss
140. relun
141. relin1
142. relin2
143. relinxp
144. reldif
145. reliun
146. reliin
147. reluni
148. relint
149. relopabiv
150. relopabv
151. relopabi
152. relopabiALT
153. relopab
154. mptrel
155. reli
156. rele
157. opabid2
158. inopab
159. difopab
160. inxp
161. xpindi
162. xpindir
163. xpiindi
164. xpriindi
165. eliunxp
166. opeliunxp2
167. raliunxp
168. rexiunxp
169. ralxp
170. rexxp
171. exopxfr
172. exopxfr2
173. djussxp
174. ralxpf
175. rexxpf
176. iunxpf
177. opabbi2dv
178. relop
179. ideqg
180. ideq
181. ididg
182. issetid
183. coss1
184. coss2
185. coeq1
186. coeq2
187. coeq1i
188. coeq2i
189. coeq1d
190. coeq2d
191. coeq12i
192. coeq12d
193. nfco
194. brcog
195. opelco2g
196. brcogw
197. eqbrrdva
198. brco
199. opelco
200. cnvss
201. cnveq
202. cnveqi
203. cnveqd
204. elcnv
205. elcnv2
206. nfcnv
207. brcnvg
208. opelcnvg
209. opelcnv
210. brcnv
211. cnv0
212. cnv0OLD
213. cnvi
214. csbcnv
215. csbcnvOLD
216. csbcnvgALTOLD
217. cnvco
218. cnvuni
219. dfdm3
220. dfrn2
221. dfrn3
222. elrn2g
223. elrng
224. elrn2
225. elrn
226. ssrelrn
227. dfdm4
228. dfdmf
229. csbdm
230. eldmg
231. eldm2g
232. eldm
233. eldm2
234. dmss
235. dmeq
236. dmeqi
237. dmeqd
238. opeldmd
239. opeldm
240. breldm
241. breldmg
242. dmun
243. dmin
244. breldmd
245. dmiun
246. dmuni
247. dmopab
248. dmopabelb
249. dmopab2rex
250. dmopabss
251. dmopab3
252. dm0
253. dmi
254. dmv
255. dmep
256. dm0rn0
257. dm0rn0OLD
258. rn0
259. rnep
260. reldm0
261. dmxp
262. dmxpid
263. dmxpin
264. xpid11
265. dmcnvcnv
266. rncnvcnv
267. elreldm
268. rneq
269. rneqi
270. rneqd
271. rnss
272. rnssi
273. brelrng
274. brelrn
275. opelrn
276. releldm
277. relelrn
278. releldmb
279. relelrnb
280. releldmi
281. relelrni
282. dfrnf
283. nfdm
284. nfrn
285. dmiin
286. rnopab
287. rnopabss
288. rnopab3
289. rnmpt
290. elrnmpt
291. elrnmpt1s
292. elrnmpt1
293. elrnmptg
294. elrnmpti
295. elrnmptd
296. elrnmpt1d
297. elrnmptdv
298. elrnmpt2d
299. nelrnmpt
300. dfiun3g
301. dfiin3g
302. dfiun3
303. dfiin3
304. riinint
305. relrn0
306. dmrnssfld
307. dmcoss
308. dmcossOLD
309. rncoss
310. dmcosseq
311. dmcosseqOLD
312. dmcoeq
313. rncoeq
314. reseq1
315. reseq2
316. reseq1i
317. reseq2i
318. reseq12i
319. reseq1d
320. reseq2d
321. reseq12d
322. nfres
323. csbres
324. res0
325. dfres3
326. opelres
327. brres
328. opelresi
329. brresi
330. opres
331. resieq
332. opelidres
333. resres
334. resundi
335. resundir
336. resindi
337. resindir
338. inres
339. resdifcom
340. resiun1
341. resiun2
342. resss
343. rescom
344. ssres
345. ssres2
346. relres
347. resabs1
348. resabs1i
349. resabs1d
350. resabs2
351. residm
352. dmresss
353. dmres
354. ssdmres
355. dmresexg
356. resima
357. resima2
358. rnresss
359. xpssres
360. elinxp
361. elres
362. elsnres
363. relssres
364. dmressnsn
365. eldmressnsn
366. eldmeldmressn
367. resdm
368. resexg
369. resexd
370. resex
371. resindm
372. resindmOLD
373. resdmdfsn
374. resdmdfsnOLD
375. reldmun
376. reldisjunOLD
377. relresdm1
378. resopab
379. iss
380. resopab2
381. resmpt
382. resmpt3
383. resmptf
384. resmptd
385. dfres2
386. mptss
387. elimampt
388. elidinxp
389. elidinxpid
390. elrid
391. idinxpres
392. idinxpresid
393. idssxp
394. opabresid
395. mptresid
396. dmresi
397. restidsing
398. iresn0n0
399. imaeq1
400. imaeq2
401. imaeq1i
402. imaeq2i
403. imaeq1d
404. imaeq2d
405. imaeq12d
406. dfima2
407. dfima3
408. elimag
409. elima
410. elima2
411. elima3
412. nfima
413. nfimad
414. imadmrn
415. imassrn
416. mptima
417. mptimass
418. imai
419. rnresi
420. resiima
421. ima0
422. 0ima
423. csbima12
424. imadisj
425. imadisjlnd
426. cnvimass
427. cnvimarndm
428. imasng
429. relimasn
430. elrelimasn
431. elimasng1
432. elimasn1
433. elimasng
434. elimasn
435. elimasni
436. args
437. elinisegg
438. eliniseg
439. epin
440. epini
441. iniseg
442. inisegn0
443. dffr3
444. dfse2
445. imass1
446. imass2
447. ndmima
448. relcnv
449. relbrcnvg
450. eliniseg2
451. relbrcnv
452. relco
453. cotrg
454. cotr
455. idrefALT
456. cnvsym
457. intasym
458. asymref
459. asymref2
460. intirr
461. brcodir
462. codir
463. qfto
464. xpidtr
465. trin2
466. poirr2
467. trinxp
468. soirri
469. sotri
470. son2lpi
471. sotri2
472. sotri3
473. poleloe
474. poltletr
475. somin1
476. somincom
477. somin2
478. soltmin
479. cnvopab
480. mptcnv
481. cnvun
482. cnvdif
483. cnvin
484. rnun
485. rnin
486. rninOLD
487. rniun
488. rnuni
489. imaundi
490. imaundir
491. cnvimassrndm
492. dminss
493. imainss
494. inimass
495. inimasn
496. cnvxp
497. cnvxpOLD
498. xp0OLD
499. xpnz
500. xpeq0
501. xpdisj1
502. xpdisj2
503. xpsndisj
504. difxp
505. difxp1
506. difxp2
507. djudisj
508. xpdifid
509. xpdifcnvepel
510. resdisj
511. rnxp
512. dmxpss
513. rnxpss
514. rnxpid
515. ssxpb
516. xp11
517. xpcan
518. xpcan2
519. ssrnres
520. rninxp
521. dminxp
522. imainrect
523. xpima
524. xpima1
525. xpima2
526. xpimasn
527. sossfld
528. sofld
529. cnvcnv3
530. dfrel2
531. dfrel4v
532. dfrel4
533. cnvcnv
534. cnvcnv2
535. cnvcnvss
536. cnvcnvssOLD
537. cnvrescnv
538. cnveqb
539. cnveq0
540. dfrel3
541. elid
542. dmresv
543. rnresv
544. dfrn4
545. imadifssran
546. imadifssranOLD
547. csbrn
548. rescnvcnv
549. cnvcnvres
550. imacnvcnv
551. dmsnn0
552. rnsnn0
553. dmsn0
554. cnvsn0
555. dmsn0el
556. relsn2
557. dmsnopg
558. dmsnopss
559. dmpropg
560. dmsnop
561. dmprop
562. dmtpop
563. cnvcnvsn
564. dmsnsnsn
565. rnsnopg
566. rnpropg
567. cnvsng
568. rnsnop
569. op1sta
570. cnvsn
571. op2ndb
572. op2nda
573. opswap
574. cnvresima
575. resdm2
576. resdmres
577. resresdm
578. imadmres
579. resdmss
580. resdifdi
581. resdifdir
582. mptpreima
583. mptiniseg
584. dmmpt
585. dmmptss
586. dmmptg
587. rnmpt0f
588. rnmptn0
589. dfco2
590. dfco2a
591. coundi
592. coundir
593. cores
594. resco
595. imaco
596. rnco
597. rncoOLD
598. rnco2
599. dmco
600. coeq0
601. coiun
602. cocnvcnv1
603. cocnvcnv2
604. cores2
605. co02
606. co01
607. coi1
608. coi2
609. coires1
610. coass
611. relcnvtrg
612. relcnvtrgOLD
613. relcnvtrOLD
614. relssdmrn
615. resssxp
616. cnvssrndm
617. cossxp
618. relrelss
619. unielrel
620. relfld
621. relresfld
622. relresfldOLD
623. relcoi2
624. relcoi1
625. unidmrn
626. relcnvfld
627. dfdm2
628. unixp
629. unixp0
630. unixpid
631. ressn
632. cnviin
633. cnvpo
634. cnvso
635. xpco
636. xpcoid
637. elsnxp
638. reu3op
639. reuop
640. opreu2reurex
641. opreu2reu
642. dfpo2
643. csbcog
644. snres0
645. imaindm
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. dffr4
22. predel
23. predtrss
24. predpo
25. predso
26. setlikespec
27. predidm
28. predin
29. predun
30. preddif
31. predep
32. trpred
33. preddowncl
34. predpoirr
35. predfrirr
36. pred0
37. dfse3
38. predrelss
39. predprc
40. 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.26i
3. wfi
4. wfii
5. wfisg
6. wfis
7. wfis2fg
8. wfis2f
9. wfis2g
10. wfis2
11. 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. ordpss
32. ordsseleq
33. ordin
34. onin
35. ordtri3or
36. ordtri1
37. ontri1
38. ordtri2
39. ordtri3
40. ordtri4
41. orddisj
42. onfr
43. onelpss
44. onsseleq
45. onelss
46. oneltri
47. ordtr1
48. ordtr2
49. ordtr3
50. ontr1
51. ontr2
52. onelssex
53. ordunidif
54. ordintdif
55. onintss
56. oneqmini
57. ord0
58. 0elon
59. ord0eln0
60. on0eln0
61. dflim2
62. inton
63. nlim0
64. limord
65. limuni
66. limuni2
67. 0ellim
68. limelon
69. onn0
70. suceqd
71. suceq
72. elsuci
73. elsucg
74. elsuc2g
75. elsuc
76. elsuc2
77. nfsuc
78. elelsuc
79. sucel
80. suc0
81. sucprc
82. unisucs
83. unisucg
84. unisuc
85. sssucid
86. sucidg
87. sucid
88. nsuceq0
89. eqelsuc
90. iunsuc
91. suctr
92. trsuc
93. trsucss
94. ordsssuc
95. onsssuc
96. ordsssuc2
97. onmindif
98. ordnbtwn
99. onnbtwn
100. sucssel
101. orddif
102. orduniss
103. ordtri2or
104. ordtri2or2
105. ordtri2or3
106. ordelinel
107. ordssun
108. ordequn
109. ordun
110. onunel
111. ordunisssuc
112. suc11
113. onun2
114. ontr
115. onunisuc
116. onordi
117. onirri
118. oneli
119. onelssi
120. onssneli
121. onssnel2i
122. onelini
123. oneluni
124. onunisuci
125. onsseli
126. onun2i
127. unizlim
128. on0eqel
129. snsn0non
130. onxpdisj
131. onnev
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. cbviota
13. cbviotav
14. sb8iota
15. iotaeq
16. iotabi
17. uniabio
18. iotaval2
19. iotauni2
20. iotanul2
21. iotaval
22. iotassuni
23. iotaex
24. iotauni
25. iotaint
26. iota1
27. iotanul
28. iota4
29. iota4an
30. iota5
31. iotabidv
32. iotabii
33. iotacl
34. iota2df
35. iota2d
36. iota2
37. iotan0
38. sniota
39. dfiota4
40. 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. dffun6
19. dffun3
20. dffun4
21. dffun5
22. dffun6f
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. fnunres1
119. fnunres2
120. fnun
121. fnund
122. fnunop
123. fncofn
124. fnco
125. fnresdm
126. fnresdisj
127. 2elresin
128. fnssresb
129. fnssres
130. fnssresd
131. fnresin1
132. fnresin2
133. fnres
134. idfn
135. fnresi
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. feq1dd
160. feq2d
161. feq3d
162. feq2dd
163. feq3dd
164. feq12d
165. feq123d
166. feq123
167. feq1i
168. feq2i
169. feq12i
170. feq23i
171. feq23d
172. nff
173. sbcfng
174. sbcfg
175. elimf
176. ffn
177. ffnd
178. dffn2
179. ffun
180. ffunOLD
181. ffund
182. frel
183. freld
184. frn
185. frnd
186. fdm
187. fdmd
188. fdmi
189. dffn3
190. ffrn
191. ffrnb
192. ffrnbd
193. fss
194. fssd
195. fssdmd
196. fssdm
197. fimass
198. fimassd
199. fimacnv
200. fcof
201. fco
202. fcod
203. fco2
204. fssxp
205. funssxp
206. ffdm
207. ffdmd
208. fdmrn
209. funcofd
210. opelf
211. fun
212. fun2
213. fun2d
214. fnfco
215. fssres
216. fssresd
217. fssres2
218. fresin
219. resasplit
220. fresaun
221. fresaunres2
222. fresaunres1
223. fcoi1
224. fcoi2
225. feu
226. fcnvres
227. fimacnvdisj
228. fint
229. fin
230. f0
231. f00
232. f0bi
233. f0dom0
234. f0rn0
235. fconst
236. fconstg
237. fnconstg
238. fconst6g
239. fconst6
240. f1eq1
241. f1eq2
242. f1eq3
243. nff1
244. dff12
245. f1f
246. f1fn
247. f1fun
248. f1funOLD
249. f1rel
250. f1relOLD
251. f1dm
252. f1ss
253. f1ssr
254. f1ssres
255. f1resf1
256. f1cnvcnv
257. f1cof1
258. f1co
259. foeq1
260. foeq2
261. foeq3
262. nffo
263. fof
264. fofun
265. fofn
266. forn
267. dffo2
268. foima
269. dffn4
270. funforn
271. fodmrnu
272. fimadmfo
273. fores
274. fimadmfoALT
275. focnvimacdmdm
276. focofo
277. foco
278. foconst
279. f1oeq1
280. f1oeq2
281. f1oeq3
282. f1oeq23
283. f1eq123d
284. foeq123d
285. f1oeq123d
286. f1oeq1d
287. f1oeq2d
288. f1oeq3d
289. nff1o
290. f1of1
291. f1of
292. f1ofn
293. f1ofun
294. f1orel
295. f1odm
296. f1odmOLD
297. dff1o2
298. dff1o3
299. f1ofo
300. dff1o4
301. dff1o5
302. f1orn
303. f1f1orn
304. f1ocnv
305. f1ocnvb
306. f1ores
307. f1orescnv
308. f1imacnv
309. foimacnv
310. foun
311. f1oun
312. f1un
313. resdif
314. resin
315. f1oco
316. f1cnv
317. funcocnv2
318. fococnv2
319. f1ococnv2
320. f1cocnv2
321. f1ococnv1
322. f1cocnv1
323. funcoeqres
324. f1ssf1
325. f10
326. f10d
327. f1o00
328. fo00
329. f1o0
330. f1oi
331. f1oiOLD
332. f1ovi
333. f1osn
334. f1osng
335. f1sng
336. fsnd
337. f1oprswap
338. f1oprg
339. tz6.12-2
340. tz6.12-2OLD
341. fveu
342. brprcneu
343. brprcneuALT
344. fvprc
345. fvprcALT
346. rnfvprc
347. fv2
348. dffv3
349. dffv4
350. elfv
351. fveq1
352. fveq2
353. fveq1i
354. fveq1d
355. fveq2i
356. fveq2d
357. 2fveq3
358. fveq12i
359. fveq12d
360. fveqeq2d
361. fveqeq2
362. nffv
363. nffvmpt1
364. nffvd
365. fvex
366. fvexi
367. fvexd
368. fvif
369. iffv
370. fv3
371. fvres
372. fvresd
373. funssfv
374. tz6.12c
375. tz6.12-1
376. tz6.12
377. tz6.12f
378. tz6.12i
379. fvbr0
380. fvrn0
381. fvn0fvelrn
382. elfvunirn
383. fvssunirn
384. ndmfv
385. ndmfvrcl
386. elfvdm
387. elfvex
388. elfvexd
389. eliman0
390. nfvres
391. nfunsn
392. fvfundmfvn0
393. 0fv
394. fv2prc
395. elfv2ex
396. fveqres
397. csbfv12
398. csbfv2g
399. csbfv
400. funbrfv
401. funopfv
402. fnbrfvb
403. fnopfvb
404. fvelima2
405. funbrfvb
406. funopfvb
407. fnbrfvb2
408. fdmeu
409. funbrfv2b
410. dffn5
411. fnrnfv
412. fvelrnb
413. foelcdmi
414. dfimafn
415. dfimafn2
416. funimass4
417. fvelima
418. funimassd
419. fvelimad
420. feqmptd
421. feqresmpt
422. feqmptdf
423. dffn5f
424. fvelimab
425. fvelimabd
426. fimarab
427. unima
428. fvi
429. fviss
430. fniinfv
431. fnsnfv
432. opabiotafun
433. opabiotadm
434. opabiota
435. fnimapr
436. fnimatpd
437. ssimaex
438. ssimaexg
439. funfv
440. funfv2
441. funfv2f
442. fvun
443. fvun1
444. fvun2
445. fvun1d
446. fvun2d
447. dffv2
448. dmfco
449. fvco2
450. fvco
451. fvcod
452. fvco3
453. fvco3d
454. fvco4i
455. fvopab3g
456. fvopab3ig
457. brfvopabrbr
458. fvmptg
459. fvmpti
460. fvmpt
461. fvmpt2f
462. funcnvmpt
463. fvtresfn
464. fvmpts
465. fvmpt3
466. fvmpt3i
467. fvmptdf
468. fvmptd
469. fvmptd2
470. mptrcl
471. fvmpt2i
472. fvmpt2
473. fvmptss
474. fvmpt2d
475. fvmptex
476. fvmptd3f
477. fvmptd2f
478. fvmptdv
479. fvmptdv2
480. mpteqb
481. fvmptt
482. fvmptf
483. fvmptnf
484. fvmptd3
485. fvmptd4
486. fvmptn
487. fvmptss2
488. elfvmptrab1w
489. elfvmptrab1
490. elfvmptrab
491. fvopab4ndm
492. fvmptndm
493. fvmptrabfv
494. fvopab5
495. fvopab6
496. eqfnfv
497. eqfnfv2
498. eqfnfv3
499. eqfnfvd
500. eqfnfv2f
501. fsneq
502. eqfunfv
503. eqfnun
504. fvreseq0
505. fvreseq1
506. fvreseq
507. fnmptfvd
508. fndmdif
509. fndmdifcom
510. fndmdifeq0
511. fndmin
512. fneqeql
513. fneqeql2
514. fnreseql
515. chfnrn
516. funfvop
517. funfvbrb
518. fvimacnvi
519. fvimacnv
520. funimass3
521. funimass5
522. funconstss
523. fvimacnvALT
524. elpreima
525. elpreimad
526. fniniseg
527. fncnvima2
528. fniniseg2
529. unpreima
530. inpreima
531. difpreima
532. respreima
533. cnvimainrn
534. sspreima
535. iunpreima
536. iinpreima
537. intpreima
538. fimacnvinrn
539. fimacnvinrn2
540. rescnvimafod
541. fvn0ssdmfun
542. fnopfv
543. fvelrn
544. nelrnfvne
545. fveqdmss
546. fveqressseq
547. fnfvelrn
548. ffvelcdm
549. fnfvelrnd
550. ffvelcdmi
551. ffvelcdmda
552. ffvelcdmd
553. feldmfvelcdm
554. rexrn
555. ralrn
556. elrnrexdm
557. elrnrexdmb
558. eldmrexrn
559. eldmrexrnb
560. fvcofneq
561. ralrnmptw
562. rexrnmptw
563. ralrnmpt
564. rexrnmpt
565. f0cli
566. dff2
567. dff3
568. dff4
569. dffo3
570. dffo4
571. dffo5
572. exfo
573. dffo3f
574. foelrn
575. foelrnf
576. foco2
577. fmpt
578. f1ompt
579. fmpti
580. fvmptelcdm
581. fmptd
582. fmpttd
583. fmpt3d
584. fmptdf
585. fompt
586. ffnfv
587. ffnfvf
588. fnfvrnss
589. fcdmssb
590. rnmptss
591. rnmptssd
592. fmpt2d
593. ffvresb
594. fssrescdmd
595. f1oresrab
596. f1ossf1o
597. fmptco
598. fmptcof
599. fmptcos
600. cofmpt
601. fcompt
602. fcoconst
603. fsn
604. fsn2
605. fsng
606. fsn2g
607. xpsng
608. xpsn
609. xpprsng
610. xpsnprg
611. xpsntpg
612. f1o2sn
613. residpr
614. dfmpt
615. fnasrn
616. idref
617. funiun
618. funopsn
619. funopsnOLD
620. funop
621. funopdmsn
622. funsndifnop
623. funsneqopb
624. ressnop0
625. fpr
626. fprg
627. ftpg
628. ftp
629. fnressn
630. funressn
631. fressnfv
632. fvrnressn
633. fvressn
634. fvconst
635. fnsnr
636. fnsnbg
637. fnsnb
638. fnsnbOLD
639. fmptsn
640. fmptsng
641. fmptsnd
642. fmptap
643. fmptapd
644. fmptpr
645. fvresi
646. fninfp
647. fnelfp
648. fndifnfp
649. fnelnfp
650. fnnfpeq0
651. fvunsn
652. fvsng
653. fvsn
654. fvsnun1
655. fvsnun2
656. fnsnsplit
657. fsnunf
658. fsnunf2
659. fsnunfv
660. fsnunres
661. funresdfunsn
662. fvpr1g
663. fvpr2g
664. fvpr1
665. fvpr2
666. fprb
667. fvtp1
668. fvtp2
669. fvtp3
670. fvtp1g
671. fvtp2g
672. fvtp3g
673. fvtp0
674. tpres
675. fvconst2g
676. fconst2g
677. fvconst2
678. fconst2
679. fconst5
680. rnmptc
681. fnprb
682. fntpb
683. fnpr2g
684. fpr2g
685. fconstfv
686. fconst3
687. fconst4
688. resfunexg
689. resiexd
690. fnex
691. fnexd
692. funex
693. opabex
694. mptexg
695. mptexgf
696. mptex
697. mptexd
698. mptrabex
699. fex
700. fexd
701. mptfvmpt
702. eufnfv
703. funfvima
704. funfvima2
705. funfvima2d
706. fnfvima
707. fnfvimad
708. resfvresima
709. funfvima3
710. ralima
711. rexima
712. fvclss
713. elabrex
714. elabrexg
715. abrexco
716. imaiun
717. imauni
718. fniunfv
719. funiunfv
720. funiunfvf
721. eluniima
722. elunirn
723. elunirnALT
724. fnunirn
725. dff13
726. dff13f
727. f1veqaeq
728. f1cofveqaeq
729. f1cofveqaeqALT
730. dff14i
731. 2f1fvneq
732. f1mpt
733. f1fveq
734. f1elima
735. f1imass
736. f1imaeq
737. f1imapss
738. fpropnf1
739. f1dom3fv3dif
740. f1dom3el3dif
741. dff14a
742. dff14b
743. dff15
744. f1resveqaeq
745. f1resrcmplf1dlem
746. f1resrcmplf1d
747. f1ounsn
748. f12dfv
749. f13dfv
750. dff1o6
751. f1ocnvfv1
752. f1ocnvfv2
753. f1ocnvfv
754. f1ocnvfvb
755. nvof1o
756. nvocnv
757. f1cdmsn
758. fsnex
759. f1prex
760. f1ocnvdm
761. f1ocnvfvrneq
762. fcof1
763. fcofo
764. cbvfo
765. cbvexfo
766. cocan1
767. cocan2
768. fcof1oinvd
769. fcof1od
770. 2fcoidinvd
771. fcof1o
772. 2fvcoidd
773. 2fvidf1od
774. 2fvidinvd
775. foeqcnvco
776. f1eqcocnv
777. fveqf1o
778. f1ocoima
779. nf1const
780. nf1oconst
781. f1ofvswap
782. fvf1pr
783. fliftrel
784. fliftel
785. fliftel1
786. fliftcnv
787. fliftfun
788. fliftfund
789. fliftfuns
790. fliftf
791. fliftval
792. isoeq1
793. isoeq2
794. isoeq3
795. isoeq4
796. isoeq5
797. nfiso
798. isof1o
799. isof1oidb
800. isof1oopb
801. isorel
802. soisores
803. soisoi
804. isoid
805. isocnv
806. isocnv2
807. isocnv3
808. isores2
809. isores1
810. isores3
811. isotr
812. isomin
813. isoini
814. isoini2
815. isofrlem
816. isoselem
817. isofr
818. isose
819. isofr2
820. isopolem
821. isopo
822. isosolem
823. isoso
824. isowe
825. isowe2
826. f1oiso
827. f1oiso2
828. f1owe
829. f1oweOLD
830. f1we
831. weniso
832. weisoeq
833. weisoeq2
834. knatar
835. fvresval
836. funeldmb
837. eqfunresadj
838. eqfunressuc
839. fnssintima
840. fnimasnd
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. nfriotad
14. nfriota
15. cbvriota
16. cbvriotav
17. csbriota
18. riotacl2
19. riotacl
20. riotasbc
21. riotabidva
22. riotabiia
23. riota1
24. riota1a
25. riota2df
26. riota2f
27. riota2
28. riotaeqimp
29. riotaprop
30. riota5f
31. riota5
32. riotass2
33. riotass
34. moriotass
35. snriota
36. riotaxfrd
37. eusvobj2
38. eusvobj1
39. f1ofveu
40. f1ocnvfv3
41. riotaund
42. riotassuni
43. riotaclb
44. riotarab
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. elfvov1
44. elfvov2
45. csbov123
46. csbov
47. csbov12g
48. csbov1g
49. csbov2g
50. rspceov
51. elovimad
52. fnbrovb
53. fnotovb
54. opabbrex
55. opabresex2
56. fvmptopab
57. f1opr
58. brfvopab
59. dfoprab2
60. reloprab
61. oprabv
62. nfoprab1
63. nfoprab2
64. nfoprab3
65. nfoprab
66. oprabbid
67. oprabbidv
68. oprabbii
69. ssoprab2
70. ssoprab2b
71. eqoprab2bw
72. eqoprab2b
73. mpoeq123
74. mpoeq12
75. mpoeq123dva
76. mpoeq123dv
77. mpoeq123i
78. mpoeq3dva
79. mpoeq3ia
80. mpoeq3dv
81. nfmpo1
82. nfmpo2
83. nfmpo
84. 0mpo0
85. mpo0v
86. mpo0
87. oprab4
88. cbvoprab1
89. cbvoprab2
90. cbvoprab12
91. cbvoprab12v
92. cbvoprab3
93. cbvoprab3v
94. cbvmpox
95. cbvmpo
96. cbvmpov
97. elimdelov
98. brif1
99. ovif
100. ovif2
101. ovif12
102. ifov
103. ifmpt2v
104. dmoprab
105. dmoprabss
106. rnoprab
107. rnoprab2
108. reldmoprab
109. oprabss
110. eloprabga
111. eloprabg
112. ssoprab2i
113. mpov
114. mpomptx
115. mpompt
116. mpodifsnif
117. mposnif
118. fconstmpo
119. resoprab
120. resoprab2
121. resmpo
122. funoprabg
123. funoprab
124. fnoprabg
125. mpofun
126. fnoprab
127. ffnov
128. fovcld
129. fovcl
130. eqfnov
131. eqfnov2
132. fnov
133. mpo2eqb
134. rnmpo
135. reldmmpo
136. elrnmpog
137. elrnmpo
138. elimampo
139. elrnmpores
140. ralrnmpo
141. rexrnmpo
142. ovid
143. ovidig
144. ovidi
145. ov
146. ovigg
147. ovig
148. ovmpt4g
149. ovmpos
150. ov2gf
151. ovmpodxf
152. ovmpodx
153. ovmpod
154. ovmpox
155. ovmpoga
156. ovmpoa
157. ovmpodf
158. ovmpodv
159. ovmpodv2
160. ovmpog
161. ovmpo
162. ovmpot
163. fvmpopr2d
164. ov3
165. ov6g
166. ovg
167. ovres
168. ovresd
169. oprres
170. ovn0ssdmfun
171. oprssov
172. fovcdm
173. fovcdmda
174. fovcdmd
175. fnrnov
176. foov
177. fnovrn
178. ovelrn
179. funimassov
180. ovelimab
181. ovima0
182. ovconst2
183. oprssdm
184. nssdmovg
185. ndmovg
186. ndmov
187. ndmovcl
188. ndmovrcl
189. ndmovcom
190. ndmovass
191. ndmovdistr
192. ndmovord
193. ndmovordi
194. Variable-to-class conversion for operations
Maps-to notation
1. mpondm0
2. elmpocl
3. elmpocl1
4. elmpocl2
5. elovmpod
6. elovmpo
7. elovmporab
8. elovmporab1w
9. elovmporab1
10. 2mpo0
11. relmptopab
12. f1ocnvd
13. f1od
14. f1ocnv2d
15. f1o2d
16. f1opw2
17. f1opw
18. elovmpt3imp
19. ovmpt3rab1
20. ovmpt3rabdm
21. elovmpt3rab1
22. 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. offvalfv
26. ofmpteq
27. coof
28. ofco
29. offveq
30. offveqb
31. ofc1
32. ofc2
33. ofc12
34. caofref
35. caofinvl
36. caofid0l
37. caofid0r
38. caofid1
39. caofid2
40. caofcom
41. caofidlcan
42. caofrss
43. caofass
44. caoftrn
45. caofdi
46. caofdir
47. 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