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. vsnex
10. snexg
11. snex
12. prex
13. exel
14. exexneq
15. exneq
16. dtru
17. el
18. sels
19. selsALT
20. elALT
21. dtruOLD
22. snelpwg
23. snelpwi
24. snelpwiOLD
25. snelpw
26. prelpw
27. prelpwi
28. rext
29. sspwb
30. unipw
31. univ
32. pwtr
33. ssextss
34. ssext
35. nssss
36. pweqb
37. intidg
38. intidOLD
39. moabex
40. rmorabex
41. euabex
42. nnullss
43. exss
44. opex
45. otex
46. elopg
47. elop
48. opi1
49. opi2
50. opeluu
51. op1stb
52. 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. copsexg
20. copsex2t
21. copsex2g
22. copsex2gOLD
23. copsex4g
24. 0nelop
25. opwo0id
26. opeqex
27. oteqex2
28. oteqex
29. opcom
30. moop2
31. opeqsng
32. opeqsn
33. opeqpr
34. snopeqop
35. propeqop
36. propssopi
37. snopeqopsnid
38. mosubopt
39. mosubop
40. euop2
41. euotd
42. opthwiener
43. uniop
44. uniopel
45. opthhausdorff
46. opthhausdorff0
47. otsndisj
48. otiunsndisj
49. iunopeqop
50. brsnop
51. 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. iunopabOLD
38. elopabr
39. elopabran
40. elopabrOLD
41. rbropapd
42. rbropap
43. 2rbropap
44. 0nelopab
45. 0nelopabOLD
46. 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
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
41. sotrine
42. 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. 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. 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. xpundi
72. xpundir
73. xpiundi
74. xpiundir
75. iunxpconst
76. xpun
77. elvv
78. elvvv
79. elvvuni
80. brinxp2
81. brinxp
82. opelinxp
83. poinxp
84. soinxp
85. frinxp
86. seinxp
87. weinxp
88. posn
89. sosn
90. frsn
91. wesn
92. elopaelxp
93. elopaelxpOLD
94. bropaex12
95. opabssxp
96. brab2a
97. optocl
98. 2optocl
99. 3optocl
100. opbrop
101. 0xp
102. csbxp
103. releq
104. releqi
105. releqd
106. nfrel
107. sbcrel
108. relss
109. ssrel
110. ssrelOLD
111. eqrel
112. ssrel2
113. ssrel3
114. relssi
115. relssdv
116. eqrelriv
117. eqrelriiv
118. eqbrriv
119. eqrelrdv
120. eqbrrdv
121. eqbrrdiv
122. eqrelrdv2
123. ssrelrel
124. eqrelrel
125. elrel
126. rel0
127. nrelv
128. relsng
129. relsnb
130. relsnopg
131. relsn
132. relsnop
133. copsex2gb
134. copsex2ga
135. elopaba
136. xpsspw
137. unixpss
138. relun
139. relin1
140. relin2
141. relinxp
142. reldif
143. reliun
144. reliin
145. reluni
146. relint
147. relopabiv
148. relopabv
149. relopabi
150. relopabiALT
151. relopab
152. mptrel
153. reli
154. rele
155. opabid2
156. inopab
157. difopab
158. difopabOLD
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. rn0
254. rnep
255. reldm0
256. dmxp
257. dmxpid
258. dmxpin
259. xpid11
260. dmcnvcnv
261. rncnvcnv
262. elreldm
263. rneq
264. rneqi
265. rneqd
266. rnss
267. rnssi
268. brelrng
269. brelrn
270. opelrn
271. releldm
272. relelrn
273. releldmb
274. relelrnb
275. releldmi
276. relelrni
277. dfrnf
278. nfdm
279. nfrn
280. dmiin
281. rnopab
282. rnmpt
283. elrnmpt
284. elrnmpt1s
285. elrnmpt1
286. elrnmptg
287. elrnmpti
288. elrnmptd
289. elrnmpt1d
290. elrnmptdv
291. elrnmpt2d
292. dfiun3g
293. dfiin3g
294. dfiun3
295. dfiin3
296. riinint
297. relrn0
298. dmrnssfld
299. dmcoss
300. rncoss
301. dmcosseq
302. dmcoeq
303. rncoeq
304. reseq1
305. reseq2
306. reseq1i
307. reseq2i
308. reseq12i
309. reseq1d
310. reseq2d
311. reseq12d
312. nfres
313. csbres
314. res0
315. dfres3
316. opelres
317. brres
318. opelresi
319. brresi
320. opres
321. resieq
322. opelidres
323. resres
324. resundi
325. resundir
326. resindi
327. resindir
328. inres
329. resdifcom
330. resiun1
331. resiun2
332. resss
333. rescom
334. ssres
335. ssres2
336. relres
337. resabs1
338. resabs1d
339. resabs2
340. residm
341. dmresss
342. dmres
343. ssdmres
344. dmresexg
345. resima
346. resima2
347. rnresss
348. xpssres
349. elinxp
350. elres
351. elsnres
352. relssres
353. dmressnsn
354. eldmressnsn
355. eldmeldmressn
356. resdm
357. resexg
358. resexd
359. resex
360. resindm
361. resdmdfsn
362. reldisjun
363. relresdm1
364. resopab
365. iss
366. resopab2
367. resmpt
368. resmpt3
369. resmptf
370. resmptd
371. dfres2
372. mptss
373. elidinxp
374. elidinxpid
375. elrid
376. idinxpres
377. idinxpresid
378. idssxp
379. opabresid
380. mptresid
381. dmresi
382. restidsing
383. iresn0n0
384. imaeq1
385. imaeq2
386. imaeq1i
387. imaeq2i
388. imaeq1d
389. imaeq2d
390. imaeq12d
391. dfima2
392. dfima3
393. elimag
394. elima
395. elima2
396. elima3
397. nfima
398. nfimad
399. imadmrn
400. imassrn
401. mptima
402. mptimass
403. imai
404. rnresi
405. resiima
406. ima0
407. 0ima
408. csbima12
409. imadisj
410. imadisjlnd
411. cnvimass
412. cnvimarndm
413. imasng
414. relimasn
415. elrelimasn
416. elimasng1
417. elimasn1
418. elimasng
419. elimasn
420. elimasngOLD
421. elimasni
422. args
423. elinisegg
424. eliniseg
425. epin
426. epini
427. iniseg
428. inisegn0
429. dffr3
430. dfse2
431. imass1
432. imass2
433. ndmima
434. relcnv
435. relbrcnvg
436. eliniseg2
437. relbrcnv
438. relco
439. cotrg
440. cotrgOLD
441. cotrgOLDOLD
442. cotr
443. idrefALT
444. cnvsym
445. cnvsymOLD
446. cnvsymOLDOLD
447. intasym
448. asymref
449. asymref2
450. intirr
451. brcodir
452. codir
453. qfto
454. xpidtr
455. trin2
456. poirr2
457. trinxp
458. soirri
459. sotri
460. son2lpi
461. sotri2
462. sotri3
463. poleloe
464. poltletr
465. somin1
466. somincom
467. somin2
468. soltmin
469. cnvopab
470. mptcnv
471. cnv0
472. cnvi
473. cnvun
474. cnvdif
475. cnvin
476. rnun
477. rnin
478. rniun
479. rnuni
480. imaundi
481. imaundir
482. cnvimassrndm
483. dminss
484. imainss
485. inimass
486. inimasn
487. cnvxp
488. xp0
489. xpnz
490. xpeq0
491. xpdisj1
492. xpdisj2
493. xpsndisj
494. difxp
495. difxp1
496. difxp2
497. djudisj
498. xpdifid
499. resdisj
500. rnxp
501. dmxpss
502. rnxpss
503. rnxpid
504. ssxpb
505. xp11
506. xpcan
507. xpcan2
508. ssrnres
509. rninxp
510. dminxp
511. imainrect
512. xpima
513. xpima1
514. xpima2
515. xpimasn
516. sossfld
517. sofld
518. cnvcnv3
519. dfrel2
520. dfrel4v
521. dfrel4
522. cnvcnv
523. cnvcnv2
524. cnvcnvss
525. cnvrescnv
526. cnveqb
527. cnveq0
528. dfrel3
529. elid
530. dmresv
531. rnresv
532. dfrn4
533. csbrn
534. rescnvcnv
535. cnvcnvres
536. imacnvcnv
537. dmsnn0
538. rnsnn0
539. dmsn0
540. cnvsn0
541. dmsn0el
542. relsn2
543. dmsnopg
544. dmsnopss
545. dmpropg
546. dmsnop
547. dmprop
548. dmtpop
549. cnvcnvsn
550. dmsnsnsn
551. rnsnopg
552. rnpropg
553. cnvsng
554. rnsnop
555. op1sta
556. cnvsn
557. op2ndb
558. op2nda
559. opswap
560. cnvresima
561. resdm2
562. resdmres
563. resresdm
564. imadmres
565. resdmss
566. resdifdi
567. resdifdir
568. mptpreima
569. mptiniseg
570. dmmpt
571. dmmptss
572. dmmptg
573. rnmpt0f
574. rnmptn0
575. dfco2
576. dfco2a
577. coundi
578. coundir
579. cores
580. resco
581. imaco
582. rnco
583. rnco2
584. dmco
585. coeq0
586. coiun
587. cocnvcnv1
588. cocnvcnv2
589. cores2
590. co02
591. co01
592. coi1
593. coi2
594. coires1
595. coass
596. relcnvtrg
597. relcnvtr
598. relssdmrn
599. relssdmrnOLD
600. resssxp
601. cnvssrndm
602. cossxp
603. relrelss
604. unielrel
605. relfld
606. relresfld
607. relcoi2
608. relcoi1
609. unidmrn
610. relcnvfld
611. dfdm2
612. unixp
613. unixp0
614. unixpid
615. ressn
616. cnviin
617. cnvpo
618. cnvso
619. xpco
620. xpcoid
621. elsnxp
622. reu3op
623. reuop
624. opreu2reurex
625. opreu2reu
626. dfpo2
627. csbcog
628. snres0
629. 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. 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. onelssex
51. ordunidif
52. ordintdif
53. onintss
54. oneqmini
55. ord0
56. 0elon
57. ord0eln0
58. on0eln0
59. dflim2
60. inton
61. nlim0
62. limord
63. limuni
64. limuni2
65. 0ellim
66. limelon
67. onn0
68. suceq
69. elsuci
70. elsucg
71. elsuc2g
72. elsuc
73. elsuc2
74. nfsuc
75. elelsuc
76. sucel
77. suc0
78. sucprc
79. unisucs
80. unisucg
81. unisuc
82. sssucid
83. sucidg
84. sucid
85. nsuceq0
86. eqelsuc
87. iunsuc
88. suctr
89. trsuc
90. trsucss
91. ordsssuc
92. onsssuc
93. ordsssuc2
94. onmindif
95. ordnbtwn
96. onnbtwn
97. sucssel
98. orddif
99. orduniss
100. ordtri2or
101. ordtri2or2
102. ordtri2or3
103. ordelinel
104. ordssun
105. ordequn
106. ordun
107. onunel
108. ordunisssuc
109. suc11
110. onun2
111. ontr
112. onunisuc
113. onordi
114. ontrciOLD
115. onirri
116. oneli
117. onelssi
118. onssneli
119. onssnel2i
120. onelini
121. oneluni
122. onunisuci
123. onsseli
124. onun2i
125. unizlim
126. on0eqel
127. snsn0non
128. onxpdisj
129. onnev
130. 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. iotaval2
20. iotauni2
21. iotanul2
22. iotaval
23. iotassuni
24. iotaex
25. iotavalOLD
26. iotauni
27. iotaint
28. iota1
29. iotanul
30. iotassuniOLD
31. iotaexOLD
32. iota4
33. iota4an
34. iota5
35. iotabidv
36. iotabii
37. iotacl
38. iota2df
39. iota2d
40. iota2
41. iotan0
42. sniota
43. dfiota4
44. 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. dffun2OLD
19. dffun2OLDOLD
20. dffun6
21. dffun3
22. dffun3OLD
23. dffun4
24. dffun5
25. dffun6f
26. dffun6OLD
27. funmo
28. funmoOLD
29. funrel
30. 0nelfun
31. funss
32. funeq
33. funeqi
34. funeqd
35. nffun
36. sbcfung
37. funeu
38. funeu2
39. dffun7
40. dffun8
41. dffun9
42. funfn
43. funfnd
44. funi
45. nfunv
46. funopg
47. funopab
48. funopabeq
49. funopab4
50. funmpt
51. funmpt2
52. funco
53. funresfunco
54. funres
55. funresd
56. funssres
57. fun2ssres
58. funun
59. fununmo
60. fununfun
61. fundif
62. funcnvsn
63. funsng
64. fnsng
65. funsn
66. funprg
67. funtpg
68. funpr
69. funtp
70. fnsn
71. fnprg
72. fntpg
73. fntp
74. funcnvpr
75. funcnvtp
76. funcnvqp
77. fun0
78. funcnv0
79. funcnvcnv
80. funcnv2
81. funcnv
82. funcnv3
83. fun2cnv
84. svrelfun
85. fncnv
86. fun11
87. fununi
88. funin
89. funres11
90. funcnvres
91. cnvresid
92. funcnvres2
93. funimacnv
94. funimass1
95. funimass2
96. imadif
97. imain
98. funimaexg
99. funimaexgOLD
100. funimaex
101. isarep1
102. isarep1OLD
103. isarep2
104. fneq1
105. fneq2
106. fneq1d
107. fneq2d
108. fneq12d
109. fneq12
110. fneq1i
111. fneq2i
112. nffn
113. fnfun
114. fnfund
115. fnrel
116. fndm
117. fndmi
118. fndmd
119. funfni
120. fndmu
121. fnbr
122. fnop
123. fneu
124. fneu2
125. fnunres1
126. fnunres2
127. fnun
128. fnund
129. fnunop
130. fncofn
131. fnco
132. fncoOLD
133. fnresdm
134. fnresdisj
135. 2elresin
136. fnssresb
137. fnssres
138. fnssresd
139. fnresin1
140. fnresin2
141. fnres
142. idfn
143. fnresi
144. fnima
145. fn0
146. fnimadisj
147. fnimaeq0
148. dfmpt3
149. mptfnf
150. fnmptf
151. fnopabg
152. fnopab
153. mptfng
154. fnmpt
155. fnmptd
156. mpt0
157. fnmpti
158. dmmpti
159. dmmptd
160. mptun
161. partfun
162. feq1
163. feq2
164. feq3
165. feq23
166. feq1d
167. feq2d
168. feq3d
169. feq12d
170. feq123d
171. feq123
172. feq1i
173. feq2i
174. feq12i
175. feq23i
176. feq23d
177. nff
178. sbcfng
179. sbcfg
180. elimf
181. ffn
182. ffnd
183. dffn2
184. ffun
185. ffund
186. frel
187. freld
188. frn
189. frnd
190. fdm
191. fdmOLD
192. fdmd
193. fdmi
194. dffn3
195. ffrn
196. ffrnb
197. ffrnbd
198. fss
199. fssd
200. fssdmd
201. fssdm
202. fimass
203. fimassd
204. fimacnv
205. fcof
206. fco
207. fcoOLD
208. fcod
209. fco2
210. fssxp
211. funssxp
212. ffdm
213. ffdmd
214. fdmrn
215. funcofd
216. fco3OLD
217. opelf
218. fun
219. fun2
220. fun2d
221. fnfco
222. fssres
223. fssresd
224. fssres2
225. fresin
226. resasplit
227. fresaun
228. fresaunres2
229. fresaunres1
230. fcoi1
231. fcoi2
232. feu
233. fcnvres
234. fimacnvdisj
235. fint
236. fin
237. f0
238. f00
239. f0bi
240. f0dom0
241. f0rn0
242. fconst
243. fconstg
244. fnconstg
245. fconst6g
246. fconst6
247. f1eq1
248. f1eq2
249. f1eq3
250. nff1
251. dff12
252. f1f
253. f1fn
254. f1fun
255. f1rel
256. f1dm
257. f1dmOLD
258. f1ss
259. f1ssr
260. f1ssres
261. f1resf1
262. f1cnvcnv
263. f1cof1
264. f1co
265. f1coOLD
266. foeq1
267. foeq2
268. foeq3
269. nffo
270. fof
271. fofun
272. fofn
273. forn
274. dffo2
275. foima
276. dffn4
277. funforn
278. fodmrnu
279. fimadmfo
280. fores
281. fimadmfoALT
282. focnvimacdmdm
283. focofo
284. foco
285. foconst
286. f1oeq1
287. f1oeq2
288. f1oeq3
289. f1oeq23
290. f1eq123d
291. foeq123d
292. f1oeq123d
293. f1oeq1d
294. f1oeq2d
295. f1oeq3d
296. nff1o
297. f1of1
298. f1of
299. f1ofn
300. f1ofun
301. f1orel
302. f1odm
303. dff1o2
304. dff1o3
305. f1ofo
306. dff1o4
307. dff1o5
308. f1orn
309. f1f1orn
310. f1ocnv
311. f1ocnvb
312. f1ores
313. f1orescnv
314. f1imacnv
315. foimacnv
316. foun
317. f1oun
318. f1un
319. resdif
320. resin
321. f1oco
322. f1cnv
323. funcocnv2
324. fococnv2
325. f1ococnv2
326. f1cocnv2
327. f1ococnv1
328. f1cocnv1
329. funcoeqres
330. f1ssf1
331. f10
332. f10d
333. f1o00
334. fo00
335. f1o0
336. f1oi
337. f1ovi
338. f1osn
339. f1osng
340. f1sng
341. fsnd
342. f1oprswap
343. f1oprg
344. tz6.12-2
345. fveu
346. brprcneu
347. brprcneuALT
348. fvprc
349. fvprcALT
350. rnfvprc
351. fv2
352. dffv3
353. dffv4
354. elfv
355. fveq1
356. fveq2
357. fveq1i
358. fveq1d
359. fveq2i
360. fveq2d
361. 2fveq3
362. fveq12i
363. fveq12d
364. fveqeq2d
365. fveqeq2
366. nffv
367. nffvmpt1
368. nffvd
369. fvex
370. fvexi
371. fvexd
372. fvif
373. iffv
374. fv3
375. fvres
376. fvresd
377. funssfv
378. tz6.12c
379. tz6.12-1
380. tz6.12-1OLD
381. tz6.12
382. tz6.12f
383. tz6.12cOLD
384. tz6.12i
385. fvbr0
386. fvrn0
387. fvn0fvelrn
388. elfvunirn
389. fvssunirn
390. fvssunirnOLD
391. ndmfv
392. ndmfvrcl
393. elfvdm
394. elfvex
395. elfvexd
396. eliman0
397. nfvres
398. nfunsn
399. fvfundmfvn0
400. 0fv
401. fv2prc
402. elfv2ex
403. fveqres
404. csbfv12
405. csbfv2g
406. csbfv
407. funbrfv
408. funopfv
409. fnbrfvb
410. fnopfvb
411. funbrfvb
412. funopfvb
413. fnbrfvb2
414. fdmeu
415. funbrfv2b
416. dffn5
417. fnrnfv
418. fvelrnb
419. foelcdmi
420. dfimafn
421. dfimafn2
422. funimass4
423. fvelima
424. funimassd
425. fvelimad
426. feqmptd
427. feqresmpt
428. feqmptdf
429. dffn5f
430. fvelimab
431. fvelimabd
432. unima
433. fvi
434. fviss
435. fniinfv
436. fnsnfv
437. fnsnfvOLD
438. opabiotafun
439. opabiotadm
440. opabiota
441. fnimapr
442. ssimaex
443. ssimaexg
444. funfv
445. funfv2
446. funfv2f
447. fvun
448. fvun1
449. fvun2
450. fvun1d
451. fvun2d
452. dffv2
453. dmfco
454. fvco2
455. fvco
456. fvco3
457. fvco3d
458. fvco4i
459. fvopab3g
460. fvopab3ig
461. brfvopabrbr
462. fvmptg
463. fvmpti
464. fvmpt
465. fvmpt2f
466. fvtresfn
467. fvmpts
468. fvmpt3
469. fvmpt3i
470. fvmptdf
471. fvmptd
472. fvmptd2
473. mptrcl
474. fvmpt2i
475. fvmpt2
476. fvmptss
477. fvmpt2d
478. fvmptex
479. fvmptd3f
480. fvmptd2f
481. fvmptdv
482. fvmptdv2
483. mpteqb
484. fvmptt
485. fvmptf
486. fvmptnf
487. fvmptd3
488. fvmptd4
489. fvmptn
490. fvmptss2
491. elfvmptrab1w
492. elfvmptrab1
493. elfvmptrab
494. fvopab4ndm
495. fvmptndm
496. fvmptrabfv
497. fvopab5
498. fvopab6
499. eqfnfv
500. eqfnfv2
501. eqfnfv3
502. eqfnfvd
503. eqfnfv2f
504. eqfunfv
505. eqfnun
506. fvreseq0
507. fvreseq1
508. fvreseq
509. fnmptfvd
510. fndmdif
511. fndmdifcom
512. fndmdifeq0
513. fndmin
514. fneqeql
515. fneqeql2
516. fnreseql
517. chfnrn
518. funfvop
519. funfvbrb
520. fvimacnvi
521. fvimacnv
522. funimass3
523. funimass5
524. funconstss
525. fvimacnvALT
526. elpreima
527. elpreimad
528. fniniseg
529. fncnvima2
530. fniniseg2
531. unpreima
532. inpreima
533. difpreima
534. respreima
535. cnvimainrn
536. sspreima
537. iinpreima
538. intpreima
539. fimacnvOLD
540. fimacnvinrn
541. fimacnvinrn2
542. rescnvimafod
543. fvn0ssdmfun
544. fnopfv
545. fvelrn
546. nelrnfvne
547. fveqdmss
548. fveqressseq
549. fnfvelrn
550. ffvelcdm
551. fnfvelrnd
552. ffvelcdmi
553. ffvelcdmda
554. ffvelcdmd
555. feldmfvelcdm
556. rexrn
557. ralrn
558. elrnrexdm
559. elrnrexdmb
560. eldmrexrn
561. eldmrexrnb
562. fvcofneq
563. ralrnmptw
564. rexrnmptw
565. ralrnmpt
566. rexrnmpt
567. f0cli
568. dff2
569. dff3
570. dff4
571. dffo3
572. dffo4
573. dffo5
574. exfo
575. dffo3f
576. foelrn
577. foelrnf
578. foco2
579. fmpt
580. f1ompt
581. fmpti
582. fvmptelcdm
583. fmptd
584. fmpttd
585. fmpt3d
586. fmptdf
587. fompt
588. ffnfv
589. ffnfvf
590. fnfvrnss
591. fcdmssb
592. rnmptss
593. fmpt2d
594. ffvresb
595. fssrescdmd
596. f1oresrab
597. f1ossf1o
598. fmptco
599. fmptcof
600. fmptcos
601. cofmpt
602. fcompt
603. fcoconst
604. fsn
605. fsn2
606. fsng
607. fsn2g
608. xpsng
609. xpprsng
610. xpsn
611. f1o2sn
612. residpr
613. dfmpt
614. fnasrn
615. idref
616. funiun
617. funopsn
618. funop
619. funopdmsn
620. funsndifnop
621. funsneqopb
622. ressnop0
623. fpr
624. fprg
625. ftpg
626. ftp
627. fnressn
628. funressn
629. fressnfv
630. fvrnressn
631. fvressn
632. fvn0fvelrnOLD
633. fvconst
634. fnsnr
635. fnsnb
636. fmptsn
637. fmptsng
638. fmptsnd
639. fmptap
640. fmptapd
641. fmptpr
642. fvresi
643. fninfp
644. fnelfp
645. fndifnfp
646. fnelnfp
647. fnnfpeq0
648. fvunsn
649. fvsng
650. fvsn
651. fvsnun1
652. fvsnun2
653. fnsnsplit
654. fsnunf
655. fsnunf2
656. fsnunfv
657. fsnunres
658. funresdfunsn
659. fvpr1g
660. fvpr2g
661. fvpr2gOLD
662. fvpr1
663. fvpr1OLD
664. fvpr2
665. fvpr2OLD
666. fprb
667. fvtp1
668. fvtp2
669. fvtp3
670. fvtp1g
671. fvtp2g
672. fvtp3g
673. tpres
674. fvconst2g
675. fconst2g
676. fvconst2
677. fconst2
678. fconst5
679. rnmptc
680. fnprb
681. fntpb
682. fnpr2g
683. fpr2g
684. fconstfv
685. fconst3
686. fconst4
687. resfunexg
688. resiexd
689. fnex
690. fnexd
691. funex
692. opabex
693. mptexg
694. mptexgf
695. mptex
696. mptexd
697. mptrabex
698. fex
699. fexd
700. mptfvmpt
701. eufnfv
702. funfvima
703. funfvima2
704. funfvima2d
705. fnfvima
706. fnfvimad
707. resfvresima
708. funfvima3
709. rexima
710. ralima
711. fvclss
712. elabrex
713. elabrexg
714. abrexco
715. imaiun
716. imauni
717. fniunfv
718. funiunfv
719. funiunfvf
720. eluniima
721. elunirn
722. elunirnALT
723. elunirn2OLD
724. fnunirn
725. dff13
726. dff13f
727. f1veqaeq
728. f1cofveqaeq
729. f1cofveqaeqALT
730. 2f1fvneq
731. f1mpt
732. f1fveq
733. f1elima
734. f1imass
735. f1imaeq
736. f1imapss
737. fpropnf1
738. f1dom3fv3dif
739. f1dom3el3dif
740. dff14a
741. dff14b
742. f12dfv
743. f13dfv
744. dff1o6
745. f1ocnvfv1
746. f1ocnvfv2
747. f1ocnvfv
748. f1ocnvfvb
749. nvof1o
750. nvocnv
751. f1cdmsn
752. fsnex
753. f1prex
754. f1ocnvdm
755. f1ocnvfvrneq
756. fcof1
757. fcofo
758. cbvfo
759. cbvexfo
760. cocan1
761. cocan2
762. fcof1oinvd
763. fcof1od
764. 2fcoidinvd
765. fcof1o
766. 2fvcoidd
767. 2fvidf1od
768. 2fvidinvd
769. foeqcnvco
770. f1eqcocnv
771. f1eqcocnvOLD
772. fveqf1o
773. nf1const
774. nf1oconst
775. f1ofvswap
776. fliftrel
777. fliftel
778. fliftel1
779. fliftcnv
780. fliftfun
781. fliftfund
782. fliftfuns
783. fliftf
784. fliftval
785. isoeq1
786. isoeq2
787. isoeq3
788. isoeq4
789. isoeq5
790. nfiso
791. isof1o
792. isof1oidb
793. isof1oopb
794. isorel
795. soisores
796. soisoi
797. isoid
798. isocnv
799. isocnv2
800. isocnv3
801. isores2
802. isores1
803. isores3
804. isotr
805. isomin
806. isoini
807. isoini2
808. isofrlem
809. isoselem
810. isofr
811. isose
812. isofr2
813. isopolem
814. isopo
815. isosolem
816. isoso
817. isowe
818. isowe2
819. f1oiso
820. f1oiso2
821. f1owe
822. weniso
823. weisoeq
824. weisoeq2
825. knatar
826. fvresval
827. funeldmb
828. eqfunresadj
829. eqfunressuc
830. fnssintima
831. imaeqsexv
832. imaeqsalv
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
45. 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. csbov123
44. csbov
45. csbov12g
46. csbov1g
47. csbov2g
48. rspceov
49. elovimad
50. fnbrovb
51. fnotovb
52. opabbrex
53. opabresex2
54. opabresex2d
55. fvmptopab
56. fvmptopabOLD
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. dmoprab
104. dmoprabss
105. rnoprab
106. rnoprab2
107. reldmoprab
108. oprabss
109. eloprabga
110. eloprabgaOLD
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. mpofunOLD
127. fnoprab
128. ffnov
129. fovcld
130. fovcl
131. eqfnov
132. eqfnov2
133. fnov
134. mpo2eqb
135. rnmpo
136. reldmmpo
137. elrnmpog
138. elrnmpo
139. elimampo
140. elrnmpores
141. ralrnmpo
142. rexrnmpo
143. ovid
144. ovidig
145. ovidi
146. ov
147. ovigg
148. ovig
149. ovmpt4g
150. ovmpos
151. ov2gf
152. ovmpodxf
153. ovmpodx
154. ovmpod
155. ovmpox
156. ovmpoga
157. ovmpoa
158. ovmpodf
159. ovmpodv
160. ovmpodv2
161. ovmpog
162. ovmpo
163. ovmpot
164. fvmpopr2d
165. ov3
166. ov6g
167. ovg
168. ovres
169. ovresd
170. oprres
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. 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