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. elOLD
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. brsnop
52. 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. opelopabg
16. brabg
17. opelopabgf
18. opelopab2
19. opelopab
20. brab
21. opelopabaf
22. opelopabf
23. ssopab2
24. ssopab2bw
25. eqopab2bw
26. ssopab2b
27. ssopab2i
28. ssopab2dv
29. eqopab2b
30. opabn0
31. opab0
32. csbopab
33. csbopabgALT
34. csbmpt12
35. csbmpt2
36. iunopab
37. elopabr
38. elopabran
39. rbropapd
40. rbropap
41. 2rbropap
42. 0nelopab
43. 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. relsng
130. relsnb
131. relsnopg
132. relsn
133. relsnop
134. copsex2gb
135. copsex2ga
136. elopaba
137. xpsspw
138. unixpss
139. relun
140. relin1
141. relin2
142. relinxp
143. reldif
144. reliun
145. reliin
146. reluni
147. relint
148. relopabiv
149. relopabv
150. relopabi
151. relopabiALT
152. relopab
153. mptrel
154. reli
155. rele
156. opabid2
157. inopab
158. difopab
159. inxp
160. inxpOLD
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. csbcnv
212. csbcnvgALT
213. cnvco
214. cnvuni
215. dfdm3
216. dfrn2
217. dfrn3
218. elrn2g
219. elrng
220. elrn2
221. elrn
222. ssrelrn
223. dfdm4
224. dfdmf
225. csbdm
226. eldmg
227. eldm2g
228. eldm
229. eldm2
230. dmss
231. dmeq
232. dmeqi
233. dmeqd
234. opeldmd
235. opeldm
236. breldm
237. breldmg
238. dmun
239. dmin
240. breldmd
241. dmiun
242. dmuni
243. dmopab
244. dmopabelb
245. dmopab2rex
246. dmopabss
247. dmopab3
248. dm0
249. dmi
250. dmv
251. dmep
252. dm0rn0
253. dm0rn0OLD
254. rn0
255. rnep
256. reldm0
257. dmxp
258. dmxpid
259. dmxpin
260. xpid11
261. dmcnvcnv
262. rncnvcnv
263. elreldm
264. rneq
265. rneqi
266. rneqd
267. rnss
268. rnssi
269. brelrng
270. brelrn
271. opelrn
272. releldm
273. relelrn
274. releldmb
275. relelrnb
276. releldmi
277. relelrni
278. dfrnf
279. nfdm
280. nfrn
281. dmiin
282. rnopab
283. rnopabss
284. rnopab3
285. rnmpt
286. elrnmpt
287. elrnmpt1s
288. elrnmpt1
289. elrnmptg
290. elrnmpti
291. elrnmptd
292. elrnmpt1d
293. elrnmptdv
294. elrnmpt2d
295. nelrnmpt
296. dfiun3g
297. dfiin3g
298. dfiun3
299. dfiin3
300. riinint
301. relrn0
302. dmrnssfld
303. dmcoss
304. dmcossOLD
305. rncoss
306. dmcosseq
307. dmcosseqOLD
308. dmcosseqOLDOLD
309. dmcoeq
310. rncoeq
311. reseq1
312. reseq2
313. reseq1i
314. reseq2i
315. reseq12i
316. reseq1d
317. reseq2d
318. reseq12d
319. nfres
320. csbres
321. res0
322. dfres3
323. opelres
324. brres
325. opelresi
326. brresi
327. opres
328. resieq
329. opelidres
330. resres
331. resundi
332. resundir
333. resindi
334. resindir
335. inres
336. resdifcom
337. resiun1
338. resiun2
339. resss
340. rescom
341. ssres
342. ssres2
343. relres
344. resabs1
345. resabs1i
346. resabs1d
347. resabs2
348. residm
349. dmresss
350. dmres
351. ssdmres
352. dmresexg
353. resima
354. resima2
355. rnresss
356. xpssres
357. elinxp
358. elres
359. elsnres
360. relssres
361. dmressnsn
362. eldmressnsn
363. eldmeldmressn
364. resdm
365. resexg
366. resexd
367. resex
368. resindm
369. resdmdfsn
370. reldisjun
371. relresdm1
372. resopab
373. iss
374. resopab2
375. resmpt
376. resmpt3
377. resmptf
378. resmptd
379. dfres2
380. mptss
381. elimampt
382. elidinxp
383. elidinxpid
384. elrid
385. idinxpres
386. idinxpresid
387. idssxp
388. opabresid
389. mptresid
390. dmresi
391. restidsing
392. iresn0n0
393. imaeq1
394. imaeq2
395. imaeq1i
396. imaeq2i
397. imaeq1d
398. imaeq2d
399. imaeq12d
400. dfima2
401. dfima3
402. elimag
403. elima
404. elima2
405. elima3
406. nfima
407. nfimad
408. imadmrn
409. imassrn
410. mptima
411. mptimass
412. imai
413. rnresi
414. resiima
415. ima0
416. 0ima
417. csbima12
418. imadisj
419. imadisjlnd
420. cnvimass
421. cnvimarndm
422. imasng
423. relimasn
424. elrelimasn
425. elimasng1
426. elimasn1
427. elimasng
428. elimasn
429. elimasni
430. args
431. elinisegg
432. eliniseg
433. epin
434. epini
435. iniseg
436. inisegn0
437. dffr3
438. dfse2
439. imass1
440. imass2
441. ndmima
442. relcnv
443. relbrcnvg
444. eliniseg2
445. relbrcnv
446. relco
447. cotrg
448. cotr
449. idrefALT
450. cnvsym
451. intasym
452. asymref
453. asymref2
454. intirr
455. brcodir
456. codir
457. qfto
458. xpidtr
459. trin2
460. poirr2
461. trinxp
462. soirri
463. sotri
464. son2lpi
465. sotri2
466. sotri3
467. poleloe
468. poltletr
469. somin1
470. somincom
471. somin2
472. soltmin
473. cnvopab
474. cnvopabOLD
475. mptcnv
476. cnv0
477. cnv0OLD
478. cnvi
479. cnvun
480. cnvdif
481. cnvin
482. rnun
483. rnin
484. rniun
485. rnuni
486. imaundi
487. imaundir
488. imadifssran
489. cnvimassrndm
490. dminss
491. imainss
492. inimass
493. inimasn
494. cnvxp
495. xp0OLD
496. xpnz
497. xpeq0
498. xpdisj1
499. xpdisj2
500. xpsndisj
501. difxp
502. difxp1
503. difxp2
504. djudisj
505. xpdifid
506. resdisj
507. rnxp
508. dmxpss
509. rnxpss
510. rnxpid
511. ssxpb
512. xp11
513. xpcan
514. xpcan2
515. ssrnres
516. rninxp
517. dminxp
518. imainrect
519. xpima
520. xpima1
521. xpima2
522. xpimasn
523. sossfld
524. sofld
525. cnvcnv3
526. dfrel2
527. dfrel4v
528. dfrel4
529. cnvcnv
530. cnvcnv2
531. cnvcnvss
532. cnvrescnv
533. cnveqb
534. cnveq0
535. dfrel3
536. elid
537. dmresv
538. rnresv
539. dfrn4
540. csbrn
541. rescnvcnv
542. cnvcnvres
543. imacnvcnv
544. dmsnn0
545. rnsnn0
546. dmsn0
547. cnvsn0
548. dmsn0el
549. relsn2
550. dmsnopg
551. dmsnopss
552. dmpropg
553. dmsnop
554. dmprop
555. dmtpop
556. cnvcnvsn
557. dmsnsnsn
558. rnsnopg
559. rnpropg
560. cnvsng
561. rnsnop
562. op1sta
563. cnvsn
564. op2ndb
565. op2nda
566. opswap
567. cnvresima
568. resdm2
569. resdmres
570. resresdm
571. imadmres
572. resdmss
573. resdifdi
574. resdifdir
575. mptpreima
576. mptiniseg
577. dmmpt
578. dmmptss
579. dmmptg
580. rnmpt0f
581. rnmptn0
582. dfco2
583. dfco2a
584. coundi
585. coundir
586. cores
587. resco
588. imaco
589. rnco
590. rncoOLD
591. rnco2
592. dmco
593. coeq0
594. coiun
595. cocnvcnv1
596. cocnvcnv2
597. cores2
598. co02
599. co01
600. coi1
601. coi2
602. coires1
603. coass
604. relcnvtrg
605. relcnvtr
606. relssdmrn
607. resssxp
608. cnvssrndm
609. cossxp
610. relrelss
611. unielrel
612. relfld
613. relresfld
614. relcoi2
615. relcoi1
616. unidmrn
617. relcnvfld
618. dfdm2
619. unixp
620. unixp0
621. unixpid
622. ressn
623. cnviin
624. cnvpo
625. cnvso
626. xpco
627. xpcoid
628. elsnxp
629. reu3op
630. reuop
631. opreu2reurex
632. opreu2reu
633. dfpo2
634. csbcog
635. snres0
636. 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. 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. oneltri
46. ordtr1
47. ordtr2
48. ordtr3
49. ontr1
50. ontr2
51. onelssex
52. ordunidif
53. ordintdif
54. onintss
55. oneqmini
56. ord0
57. 0elon
58. ord0eln0
59. on0eln0
60. dflim2
61. inton
62. nlim0
63. limord
64. limuni
65. limuni2
66. 0ellim
67. limelon
68. onn0
69. suceqd
70. suceq
71. elsuci
72. elsucg
73. elsuc2g
74. elsuc
75. elsuc2
76. nfsuc
77. elelsuc
78. sucel
79. suc0
80. sucprc
81. unisucs
82. unisucg
83. unisuc
84. sssucid
85. sucidg
86. sucid
87. nsuceq0
88. eqelsuc
89. iunsuc
90. suctr
91. trsuc
92. trsucss
93. ordsssuc
94. onsssuc
95. ordsssuc2
96. onmindif
97. ordnbtwn
98. onnbtwn
99. sucssel
100. orddif
101. orduniss
102. ordtri2or
103. ordtri2or2
104. ordtri2or3
105. ordelinel
106. ordssun
107. ordequn
108. ordun
109. onunel
110. ordunisssuc
111. suc11
112. onun2
113. ontr
114. onunisuc
115. onordi
116. onirri
117. oneli
118. onelssi
119. onssneli
120. onssnel2i
121. onelini
122. oneluni
123. onunisuci
124. onsseli
125. onun2i
126. unizlim
127. on0eqel
128. snsn0non
129. onxpdisj
130. 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. f1imadifssran
94. funimaexg
95. funimaex
96. isarep1
97. isarep2
98. fneq1
99. fneq2
100. fneq1d
101. fneq2d
102. fneq12d
103. fneq12
104. fneq1i
105. fneq2i
106. nffn
107. fnfun
108. fnfund
109. fnrel
110. fndm
111. fndmi
112. fndmd
113. funfni
114. fndmu
115. fnbr
116. fnop
117. fneu
118. fneu2
119. fnunres1
120. fnunres2
121. fnun
122. fnund
123. fnunop
124. fncofn
125. fnco
126. fnresdm
127. fnresdisj
128. 2elresin
129. fnssresb
130. fnssres
131. fnssresd
132. fnresin1
133. fnresin2
134. fnres
135. idfn
136. fnresi
137. fnima
138. fn0
139. fnimadisj
140. fnimaeq0
141. dfmpt3
142. mptfnf
143. fnmptf
144. fnopabg
145. fnopab
146. mptfng
147. fnmpt
148. fnmptd
149. mpt0
150. fnmpti
151. dmmpti
152. dmmptd
153. mptun
154. partfun
155. feq1
156. feq2
157. feq3
158. feq23
159. feq1d
160. feq1dd
161. feq2d
162. feq3d
163. feq2dd
164. feq3dd
165. feq12d
166. feq123d
167. feq123
168. feq1i
169. feq2i
170. feq12i
171. feq23i
172. feq23d
173. nff
174. sbcfng
175. sbcfg
176. elimf
177. ffn
178. ffnd
179. dffn2
180. ffun
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. f1rel
249. f1dm
250. f1ss
251. f1ssr
252. f1ssres
253. f1resf1
254. f1cnvcnv
255. f1cof1
256. f1co
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. f1un
310. resdif
311. resin
312. f1oco
313. f1cnv
314. funcocnv2
315. fococnv2
316. f1ococnv2
317. f1cocnv2
318. f1ococnv1
319. f1cocnv1
320. funcoeqres
321. f1ssf1
322. f10
323. f10d
324. f1o00
325. fo00
326. f1o0
327. f1oi
328. f1oiOLD
329. f1ovi
330. f1osn
331. f1osng
332. f1sng
333. fsnd
334. f1oprswap
335. f1oprg
336. tz6.12-2
337. tz6.12-2OLD
338. fveu
339. brprcneu
340. brprcneuALT
341. fvprc
342. fvprcALT
343. rnfvprc
344. fv2
345. dffv3
346. dffv4
347. elfv
348. fveq1
349. fveq2
350. fveq1i
351. fveq1d
352. fveq2i
353. fveq2d
354. 2fveq3
355. fveq12i
356. fveq12d
357. fveqeq2d
358. fveqeq2
359. nffv
360. nffvmpt1
361. nffvd
362. fvex
363. fvexi
364. fvexd
365. fvif
366. iffv
367. fv3
368. fvres
369. fvresd
370. funssfv
371. tz6.12c
372. tz6.12-1
373. tz6.12
374. tz6.12f
375. tz6.12i
376. fvbr0
377. fvrn0
378. fvn0fvelrn
379. elfvunirn
380. fvssunirn
381. ndmfv
382. ndmfvrcl
383. elfvdm
384. elfvex
385. elfvexd
386. eliman0
387. nfvres
388. nfunsn
389. fvfundmfvn0
390. 0fv
391. fv2prc
392. elfv2ex
393. fveqres
394. csbfv12
395. csbfv2g
396. csbfv
397. funbrfv
398. funopfv
399. fnbrfvb
400. fnopfvb
401. fvelima2
402. funbrfvb
403. funopfvb
404. fnbrfvb2
405. fdmeu
406. funbrfv2b
407. dffn5
408. fnrnfv
409. fvelrnb
410. foelcdmi
411. dfimafn
412. dfimafn2
413. funimass4
414. fvelima
415. funimassd
416. fvelimad
417. feqmptd
418. feqresmpt
419. feqmptdf
420. dffn5f
421. fvelimab
422. fvelimabd
423. fimarab
424. unima
425. fvi
426. fviss
427. fniinfv
428. fnsnfv
429. opabiotafun
430. opabiotadm
431. opabiota
432. fnimapr
433. fnimatpd
434. ssimaex
435. ssimaexg
436. funfv
437. funfv2
438. funfv2f
439. fvun
440. fvun1
441. fvun2
442. fvun1d
443. fvun2d
444. dffv2
445. dmfco
446. fvco2
447. fvco
448. fvco3
449. fvco3d
450. fvco4i
451. fvopab3g
452. fvopab3ig
453. brfvopabrbr
454. fvmptg
455. fvmpti
456. fvmpt
457. fvmpt2f
458. funcnvmpt
459. fvtresfn
460. fvmpts
461. fvmpt3
462. fvmpt3i
463. fvmptdf
464. fvmptd
465. fvmptd2
466. mptrcl
467. fvmpt2i
468. fvmpt2
469. fvmptss
470. fvmpt2d
471. fvmptex
472. fvmptd3f
473. fvmptd2f
474. fvmptdv
475. fvmptdv2
476. mpteqb
477. fvmptt
478. fvmptf
479. fvmptnf
480. fvmptd3
481. fvmptd4
482. fvmptn
483. fvmptss2
484. elfvmptrab1w
485. elfvmptrab1
486. elfvmptrab
487. fvopab4ndm
488. fvmptndm
489. fvmptrabfv
490. fvopab5
491. fvopab6
492. eqfnfv
493. eqfnfv2
494. eqfnfv3
495. eqfnfvd
496. eqfnfv2f
497. eqfunfv
498. eqfnun
499. fvreseq0
500. fvreseq1
501. fvreseq
502. fnmptfvd
503. fndmdif
504. fndmdifcom
505. fndmdifeq0
506. fndmin
507. fneqeql
508. fneqeql2
509. fnreseql
510. chfnrn
511. funfvop
512. funfvbrb
513. fvimacnvi
514. fvimacnv
515. funimass3
516. funimass5
517. funconstss
518. fvimacnvALT
519. elpreima
520. elpreimad
521. fniniseg
522. fncnvima2
523. fniniseg2
524. unpreima
525. inpreima
526. difpreima
527. respreima
528. cnvimainrn
529. sspreima
530. iinpreima
531. intpreima
532. fimacnvinrn
533. fimacnvinrn2
534. rescnvimafod
535. fvn0ssdmfun
536. fnopfv
537. fvelrn
538. nelrnfvne
539. fveqdmss
540. fveqressseq
541. fnfvelrn
542. ffvelcdm
543. fnfvelrnd
544. ffvelcdmi
545. ffvelcdmda
546. ffvelcdmd
547. feldmfvelcdm
548. rexrn
549. ralrn
550. elrnrexdm
551. elrnrexdmb
552. eldmrexrn
553. eldmrexrnb
554. fvcofneq
555. ralrnmptw
556. rexrnmptw
557. ralrnmpt
558. rexrnmpt
559. f0cli
560. dff2
561. dff3
562. dff4
563. dffo3
564. dffo4
565. dffo5
566. exfo
567. dffo3f
568. foelrn
569. foelrnf
570. foco2
571. fmpt
572. f1ompt
573. fmpti
574. fvmptelcdm
575. fmptd
576. fmpttd
577. fmpt3d
578. fmptdf
579. fompt
580. ffnfv
581. ffnfvf
582. fnfvrnss
583. fcdmssb
584. rnmptss
585. rnmptssd
586. fmpt2d
587. ffvresb
588. fssrescdmd
589. f1oresrab
590. f1ossf1o
591. fmptco
592. fmptcof
593. fmptcos
594. cofmpt
595. fcompt
596. fcoconst
597. fsn
598. fsn2
599. fsng
600. fsn2g
601. xpsng
602. xpprsng
603. xpsn
604. f1o2sn
605. residpr
606. dfmpt
607. fnasrn
608. idref
609. funiun
610. funopsn
611. funop
612. funopdmsn
613. funsndifnop
614. funsneqopb
615. ressnop0
616. fpr
617. fprg
618. ftpg
619. ftp
620. fnressn
621. funressn
622. fressnfv
623. fvrnressn
624. fvressn
625. fvconst
626. fnsnr
627. fnsnbg
628. fnsnb
629. fnsnbOLD
630. fmptsn
631. fmptsng
632. fmptsnd
633. fmptap
634. fmptapd
635. fmptpr
636. fvresi
637. fninfp
638. fnelfp
639. fndifnfp
640. fnelnfp
641. fnnfpeq0
642. fvunsn
643. fvsng
644. fvsn
645. fvsnun1
646. fvsnun2
647. fnsnsplit
648. fsnunf
649. fsnunf2
650. fsnunfv
651. fsnunres
652. funresdfunsn
653. fvpr1g
654. fvpr2g
655. fvpr1
656. fvpr2
657. fprb
658. fvtp1
659. fvtp2
660. fvtp3
661. fvtp1g
662. fvtp2g
663. fvtp3g
664. tpres
665. fvconst2g
666. fconst2g
667. fvconst2
668. fconst2
669. fconst5
670. rnmptc
671. fnprb
672. fntpb
673. fnpr2g
674. fpr2g
675. fconstfv
676. fconst3
677. fconst4
678. resfunexg
679. resiexd
680. fnex
681. fnexd
682. funex
683. opabex
684. mptexg
685. mptexgf
686. mptex
687. mptexd
688. mptrabex
689. fex
690. fexd
691. mptfvmpt
692. eufnfv
693. funfvima
694. funfvima2
695. funfvima2d
696. fnfvima
697. fnfvimad
698. resfvresima
699. funfvima3
700. ralima
701. rexima
702. reximaOLD
703. ralimaOLD
704. fvclss
705. elabrex
706. elabrexg
707. abrexco
708. imaiun
709. imauni
710. fniunfv
711. funiunfv
712. funiunfvf
713. eluniima
714. elunirn
715. elunirnALT
716. fnunirn
717. dff13
718. dff13f
719. f1veqaeq
720. f1cofveqaeq
721. f1cofveqaeqALT
722. dff14i
723. 2f1fvneq
724. f1mpt
725. f1fveq
726. f1elima
727. f1imass
728. f1imaeq
729. f1imapss
730. fpropnf1
731. f1dom3fv3dif
732. f1dom3el3dif
733. dff14a
734. dff14b
735. f1ounsn
736. f12dfv
737. f13dfv
738. dff1o6
739. f1ocnvfv1
740. f1ocnvfv2
741. f1ocnvfv
742. f1ocnvfvb
743. nvof1o
744. nvocnv
745. f1cdmsn
746. fsnex
747. f1prex
748. f1ocnvdm
749. f1ocnvfvrneq
750. fcof1
751. fcofo
752. cbvfo
753. cbvexfo
754. cocan1
755. cocan2
756. fcof1oinvd
757. fcof1od
758. 2fcoidinvd
759. fcof1o
760. 2fvcoidd
761. 2fvidf1od
762. 2fvidinvd
763. foeqcnvco
764. f1eqcocnv
765. fveqf1o
766. f1ocoima
767. nf1const
768. nf1oconst
769. f1ofvswap
770. fvf1pr
771. fliftrel
772. fliftel
773. fliftel1
774. fliftcnv
775. fliftfun
776. fliftfund
777. fliftfuns
778. fliftf
779. fliftval
780. isoeq1
781. isoeq2
782. isoeq3
783. isoeq4
784. isoeq5
785. nfiso
786. isof1o
787. isof1oidb
788. isof1oopb
789. isorel
790. soisores
791. soisoi
792. isoid
793. isocnv
794. isocnv2
795. isocnv3
796. isores2
797. isores1
798. isores3
799. isotr
800. isomin
801. isoini
802. isoini2
803. isofrlem
804. isoselem
805. isofr
806. isose
807. isofr2
808. isopolem
809. isopo
810. isosolem
811. isoso
812. isowe
813. isowe2
814. f1oiso
815. f1oiso2
816. f1owe
817. weniso
818. weisoeq
819. weisoeq2
820. knatar
821. fvresval
822. funeldmb
823. eqfunresadj
824. eqfunressuc
825. fnssintima
826. imaeqsexvOLD
827. imaeqsalvOLD
828. 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. oprssov
171. fovcdm
172. fovcdmda
173. fovcdmd
174. fnrnov
175. foov
176. fnovrn
177. ovelrn
178. funimassov
179. ovelimab
180. ovima0
181. ovconst2
182. oprssdm
183. nssdmovg
184. ndmovg
185. ndmov
186. ndmovcl
187. ndmovrcl
188. ndmovcom
189. ndmovass
190. ndmovdistr
191. ndmovord
192. ndmovordi
193. 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