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. xpindi
161. xpindir
162. xpiindi
163. xpriindi
164. eliunxp
165. opeliunxp2
166. raliunxp
167. rexiunxp
168. ralxp
169. rexxp
170. exopxfr
171. exopxfr2
172. djussxp
173. ralxpf
174. rexxpf
175. iunxpf
176. opabbi2dv
177. relop
178. ideqg
179. ideq
180. ididg
181. issetid
182. coss1
183. coss2
184. coeq1
185. coeq2
186. coeq1i
187. coeq2i
188. coeq1d
189. coeq2d
190. coeq12i
191. coeq12d
192. nfco
193. brcog
194. opelco2g
195. brcogw
196. eqbrrdva
197. brco
198. opelco
199. cnvss
200. cnveq
201. cnveqi
202. cnveqd
203. elcnv
204. elcnv2
205. nfcnv
206. brcnvg
207. opelcnvg
208. opelcnv
209. brcnv
210. csbcnv
211. csbcnvgALT
212. cnvco
213. cnvuni
214. dfdm3
215. dfrn2
216. dfrn3
217. elrn2g
218. elrng
219. elrn2
220. elrn
221. ssrelrn
222. dfdm4
223. dfdmf
224. csbdm
225. eldmg
226. eldm2g
227. eldm
228. eldm2
229. dmss
230. dmeq
231. dmeqi
232. dmeqd
233. opeldmd
234. opeldm
235. breldm
236. breldmg
237. dmun
238. dmin
239. breldmd
240. dmiun
241. dmuni
242. dmopab
243. dmopabelb
244. dmopab2rex
245. dmopabss
246. dmopab3
247. dm0
248. dmi
249. dmv
250. dmep
251. dm0rn0
252. rn0
253. rnep
254. reldm0
255. dmxp
256. dmxpid
257. dmxpin
258. xpid11
259. dmcnvcnv
260. rncnvcnv
261. elreldm
262. rneq
263. rneqi
264. rneqd
265. rnss
266. rnssi
267. brelrng
268. brelrn
269. opelrn
270. releldm
271. relelrn
272. releldmb
273. relelrnb
274. releldmi
275. relelrni
276. dfrnf
277. nfdm
278. nfrn
279. dmiin
280. rnopab
281. rnmpt
282. elrnmpt
283. elrnmpt1s
284. elrnmpt1
285. elrnmptg
286. elrnmpti
287. elrnmptd
288. elrnmptdv
289. elrnmpt2d
290. dfiun3g
291. dfiin3g
292. dfiun3
293. dfiin3
294. riinint
295. relrn0
296. dmrnssfld
297. dmcoss
298. rncoss
299. dmcosseq
300. dmcoeq
301. rncoeq
302. reseq1
303. reseq2
304. reseq1i
305. reseq2i
306. reseq12i
307. reseq1d
308. reseq2d
309. reseq12d
310. nfres
311. csbres
312. res0
313. dfres3
314. opelres
315. brres
316. opelresi
317. brresi
318. opres
319. resieq
320. opelidres
321. resres
322. resundi
323. resundir
324. resindi
325. resindir
326. inres
327. resdifcom
328. resiun1
329. resiun2
330. dmres
331. ssdmres
332. dmresexg
333. resss
334. rescom
335. ssres
336. ssres2
337. relres
338. resabs1
339. resabs1d
340. resabs2
341. residm
342. resima
343. resima2
344. rnresss
345. xpssres
346. elinxp
347. elres
348. elsnres
349. relssres
350. dmressnsn
351. eldmressnsn
352. eldmeldmressn
353. resdm
354. resexg
355. resexd
356. resex
357. resindm
358. resdmdfsn
359. reldisjun
360. relresdm1
361. resopab
362. iss
363. resopab2
364. resmpt
365. resmpt3
366. resmptf
367. resmptd
368. dfres2
369. mptss
370. elidinxp
371. elidinxpid
372. elrid
373. idinxpres
374. idinxpresid
375. idssxp
376. opabresid
377. mptresid
378. dmresi
379. restidsing
380. iresn0n0
381. imaeq1
382. imaeq2
383. imaeq1i
384. imaeq2i
385. imaeq1d
386. imaeq2d
387. imaeq12d
388. dfima2
389. dfima3
390. elimag
391. elima
392. elima2
393. elima3
394. nfima
395. nfimad
396. imadmrn
397. imassrn
398. mptima
399. mptimass
400. imai
401. rnresi
402. resiima
403. ima0
404. 0ima
405. csbima12
406. imadisj
407. cnvimass
408. cnvimarndm
409. imasng
410. relimasn
411. elrelimasn
412. elimasng1
413. elimasn1
414. elimasng
415. elimasn
416. elimasngOLD
417. elimasni
418. args
419. elinisegg
420. eliniseg
421. epin
422. epini
423. iniseg
424. inisegn0
425. dffr3
426. dfse2
427. imass1
428. imass2
429. ndmima
430. relcnv
431. relbrcnvg
432. eliniseg2
433. relbrcnv
434. relco
435. cotrg
436. cotrgOLD
437. cotrgOLDOLD
438. cotr
439. idrefALT
440. cnvsym
441. cnvsymOLD
442. cnvsymOLDOLD
443. intasym
444. asymref
445. asymref2
446. intirr
447. brcodir
448. codir
449. qfto
450. xpidtr
451. trin2
452. poirr2
453. trinxp
454. soirri
455. sotri
456. son2lpi
457. sotri2
458. sotri3
459. poleloe
460. poltletr
461. somin1
462. somincom
463. somin2
464. soltmin
465. cnvopab
466. mptcnv
467. cnv0
468. cnvi
469. cnvun
470. cnvdif
471. cnvin
472. rnun
473. rnin
474. rniun
475. rnuni
476. imaundi
477. imaundir
478. cnvimassrndm
479. dminss
480. imainss
481. inimass
482. inimasn
483. cnvxp
484. xp0
485. xpnz
486. xpeq0
487. xpdisj1
488. xpdisj2
489. xpsndisj
490. difxp
491. difxp1
492. difxp2
493. djudisj
494. xpdifid
495. resdisj
496. rnxp
497. dmxpss
498. rnxpss
499. rnxpid
500. ssxpb
501. xp11
502. xpcan
503. xpcan2
504. ssrnres
505. rninxp
506. dminxp
507. imainrect
508. xpima
509. xpima1
510. xpima2
511. xpimasn
512. sossfld
513. sofld
514. cnvcnv3
515. dfrel2
516. dfrel4v
517. dfrel4
518. cnvcnv
519. cnvcnv2
520. cnvcnvss
521. cnvrescnv
522. cnveqb
523. cnveq0
524. dfrel3
525. elid
526. dmresv
527. rnresv
528. dfrn4
529. csbrn
530. rescnvcnv
531. cnvcnvres
532. imacnvcnv
533. dmsnn0
534. rnsnn0
535. dmsn0
536. cnvsn0
537. dmsn0el
538. relsn2
539. dmsnopg
540. dmsnopss
541. dmpropg
542. dmsnop
543. dmprop
544. dmtpop
545. cnvcnvsn
546. dmsnsnsn
547. rnsnopg
548. rnpropg
549. cnvsng
550. rnsnop
551. op1sta
552. cnvsn
553. op2ndb
554. op2nda
555. opswap
556. cnvresima
557. resdm2
558. resdmres
559. resresdm
560. imadmres
561. resdmss
562. resdifdi
563. resdifdir
564. mptpreima
565. mptiniseg
566. dmmpt
567. dmmptss
568. dmmptg
569. rnmpt0f
570. rnmptn0
571. dfco2
572. dfco2a
573. coundi
574. coundir
575. cores
576. resco
577. imaco
578. rnco
579. rnco2
580. dmco
581. coeq0
582. coiun
583. cocnvcnv1
584. cocnvcnv2
585. cores2
586. co02
587. co01
588. coi1
589. coi2
590. coires1
591. coass
592. relcnvtrg
593. relcnvtr
594. relssdmrn
595. relssdmrnOLD
596. resssxp
597. cnvssrndm
598. cossxp
599. relrelss
600. unielrel
601. relfld
602. relresfld
603. relcoi2
604. relcoi1
605. unidmrn
606. relcnvfld
607. dfdm2
608. unixp
609. unixp0
610. unixpid
611. ressn
612. cnviin
613. cnvpo
614. cnvso
615. xpco
616. xpcoid
617. elsnxp
618. reu3op
619. reuop
620. opreu2reurex
621. opreu2reu
622. dfpo2
623. csbcog
624. snres0
625. 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. fimacnv
204. fcof
205. fco
206. fcoOLD
207. fcod
208. fco2
209. fssxp
210. funssxp
211. ffdm
212. ffdmd
213. fdmrn
214. funcofd
215. fco3OLD
216. opelf
217. fun
218. fun2
219. fun2d
220. fnfco
221. fssres
222. fssresd
223. fssres2
224. fresin
225. resasplit
226. fresaun
227. fresaunres2
228. fresaunres1
229. fcoi1
230. fcoi2
231. feu
232. fcnvres
233. fimacnvdisj
234. fint
235. fin
236. f0
237. f00
238. f0bi
239. f0dom0
240. f0rn0
241. fconst
242. fconstg
243. fnconstg
244. fconst6g
245. fconst6
246. f1eq1
247. f1eq2
248. f1eq3
249. nff1
250. dff12
251. f1f
252. f1fn
253. f1fun
254. f1rel
255. f1dm
256. f1dmOLD
257. f1ss
258. f1ssr
259. f1ssres
260. f1resf1
261. f1cnvcnv
262. f1cof1
263. f1co
264. f1coOLD
265. foeq1
266. foeq2
267. foeq3
268. nffo
269. fof
270. fofun
271. fofn
272. forn
273. dffo2
274. foima
275. dffn4
276. funforn
277. fodmrnu
278. fimadmfo
279. fores
280. fimadmfoALT
281. focnvimacdmdm
282. focofo
283. foco
284. foconst
285. f1oeq1
286. f1oeq2
287. f1oeq3
288. f1oeq23
289. f1eq123d
290. foeq123d
291. f1oeq123d
292. f1oeq1d
293. f1oeq2d
294. f1oeq3d
295. nff1o
296. f1of1
297. f1of
298. f1ofn
299. f1ofun
300. f1orel
301. f1odm
302. dff1o2
303. dff1o3
304. f1ofo
305. dff1o4
306. dff1o5
307. f1orn
308. f1f1orn
309. f1ocnv
310. f1ocnvb
311. f1ores
312. f1orescnv
313. f1imacnv
314. foimacnv
315. foun
316. f1oun
317. f1un
318. resdif
319. resin
320. f1oco
321. f1cnv
322. funcocnv2
323. fococnv2
324. f1ococnv2
325. f1cocnv2
326. f1ococnv1
327. f1cocnv1
328. funcoeqres
329. f1ssf1
330. f10
331. f10d
332. f1o00
333. fo00
334. f1o0
335. f1oi
336. f1ovi
337. f1osn
338. f1osng
339. f1sng
340. fsnd
341. f1oprswap
342. f1oprg
343. tz6.12-2
344. fveu
345. brprcneu
346. brprcneuALT
347. fvprc
348. fvprcALT
349. rnfvprc
350. fv2
351. dffv3
352. dffv4
353. elfv
354. fveq1
355. fveq2
356. fveq1i
357. fveq1d
358. fveq2i
359. fveq2d
360. 2fveq3
361. fveq12i
362. fveq12d
363. fveqeq2d
364. fveqeq2
365. nffv
366. nffvmpt1
367. nffvd
368. fvex
369. fvexi
370. fvexd
371. fvif
372. iffv
373. fv3
374. fvres
375. fvresd
376. funssfv
377. tz6.12c
378. tz6.12-1
379. tz6.12-1OLD
380. tz6.12
381. tz6.12f
382. tz6.12cOLD
383. tz6.12i
384. fvbr0
385. fvrn0
386. fvn0fvelrn
387. elfvunirn
388. fvssunirn
389. fvssunirnOLD
390. ndmfv
391. ndmfvrcl
392. elfvdm
393. elfvex
394. elfvexd
395. eliman0
396. nfvres
397. nfunsn
398. fvfundmfvn0
399. 0fv
400. fv2prc
401. elfv2ex
402. fveqres
403. csbfv12
404. csbfv2g
405. csbfv
406. funbrfv
407. funopfv
408. fnbrfvb
409. fnopfvb
410. funbrfvb
411. funopfvb
412. fnbrfvb2
413. funbrfv2b
414. dffn5
415. fnrnfv
416. fvelrnb
417. foelcdmi
418. dfimafn
419. dfimafn2
420. funimass4
421. fvelima
422. funimassd
423. fvelimad
424. feqmptd
425. feqresmpt
426. feqmptdf
427. dffn5f
428. fvelimab
429. fvelimabd
430. unima
431. fvi
432. fviss
433. fniinfv
434. fnsnfv
435. fnsnfvOLD
436. opabiotafun
437. opabiotadm
438. opabiota
439. fnimapr
440. ssimaex
441. ssimaexg
442. funfv
443. funfv2
444. funfv2f
445. fvun
446. fvun1
447. fvun2
448. fvun1d
449. fvun2d
450. dffv2
451. dmfco
452. fvco2
453. fvco
454. fvco3
455. fvco3d
456. fvco4i
457. fvopab3g
458. fvopab3ig
459. brfvopabrbr
460. fvmptg
461. fvmpti
462. fvmpt
463. fvmpt2f
464. fvtresfn
465. fvmpts
466. fvmpt3
467. fvmpt3i
468. fvmptdf
469. fvmptd
470. fvmptd2
471. mptrcl
472. fvmpt2i
473. fvmpt2
474. fvmptss
475. fvmpt2d
476. fvmptex
477. fvmptd3f
478. fvmptd2f
479. fvmptdv
480. fvmptdv2
481. mpteqb
482. fvmptt
483. fvmptf
484. fvmptnf
485. fvmptd3
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. eqfunfv
502. eqfnun
503. fvreseq0
504. fvreseq1
505. fvreseq
506. fnmptfvd
507. fndmdif
508. fndmdifcom
509. fndmdifeq0
510. fndmin
511. fneqeql
512. fneqeql2
513. fnreseql
514. chfnrn
515. funfvop
516. funfvbrb
517. fvimacnvi
518. fvimacnv
519. funimass3
520. funimass5
521. funconstss
522. fvimacnvALT
523. elpreima
524. elpreimad
525. fniniseg
526. fncnvima2
527. fniniseg2
528. unpreima
529. inpreima
530. difpreima
531. respreima
532. cnvimainrn
533. sspreima
534. iinpreima
535. intpreima
536. fimacnvOLD
537. fimacnvinrn
538. fimacnvinrn2
539. rescnvimafod
540. fvn0ssdmfun
541. fnopfv
542. fvelrn
543. nelrnfvne
544. fveqdmss
545. fveqressseq
546. fnfvelrn
547. ffvelcdm
548. fnfvelrnd
549. ffvelcdmi
550. ffvelcdmda
551. ffvelcdmd
552. rexrn
553. ralrn
554. elrnrexdm
555. elrnrexdmb
556. eldmrexrn
557. eldmrexrnb
558. fvcofneq
559. ralrnmptw
560. rexrnmptw
561. ralrnmpt
562. rexrnmpt
563. f0cli
564. dff2
565. dff3
566. dff4
567. dffo3
568. dffo4
569. dffo5
570. exfo
571. dffo3f
572. foelrn
573. foelrnf
574. foco2
575. fmpt
576. f1ompt
577. fmpti
578. fvmptelcdm
579. fmptd
580. fmpttd
581. fmpt3d
582. fmptdf
583. fompt
584. ffnfv
585. ffnfvf
586. fnfvrnss
587. fcdmssb
588. rnmptss
589. fmpt2d
590. ffvresb
591. f1oresrab
592. f1ossf1o
593. fmptco
594. fmptcof
595. fmptcos
596. cofmpt
597. fcompt
598. fcoconst
599. fsn
600. fsn2
601. fsng
602. fsn2g
603. xpsng
604. xpprsng
605. xpsn
606. f1o2sn
607. residpr
608. dfmpt
609. fnasrn
610. idref
611. funiun
612. funopsn
613. funop
614. funopdmsn
615. funsndifnop
616. funsneqopb
617. ressnop0
618. fpr
619. fprg
620. ftpg
621. ftp
622. fnressn
623. funressn
624. fressnfv
625. fvrnressn
626. fvressn
627. fvn0fvelrnOLD
628. fvconst
629. fnsnr
630. fnsnb
631. fmptsn
632. fmptsng
633. fmptsnd
634. fmptap
635. fmptapd
636. fmptpr
637. fvresi
638. fninfp
639. fnelfp
640. fndifnfp
641. fnelnfp
642. fnnfpeq0
643. fvunsn
644. fvsng
645. fvsn
646. fvsnun1
647. fvsnun2
648. fnsnsplit
649. fsnunf
650. fsnunf2
651. fsnunfv
652. fsnunres
653. funresdfunsn
654. fvpr1g
655. fvpr2g
656. fvpr2gOLD
657. fvpr1
658. fvpr1OLD
659. fvpr2
660. fvpr2OLD
661. fprb
662. fvtp1
663. fvtp2
664. fvtp3
665. fvtp1g
666. fvtp2g
667. fvtp3g
668. tpres
669. fvconst2g
670. fconst2g
671. fvconst2
672. fconst2
673. fconst5
674. rnmptc
675. fnprb
676. fntpb
677. fnpr2g
678. fpr2g
679. fconstfv
680. fconst3
681. fconst4
682. resfunexg
683. resiexd
684. fnex
685. fnexd
686. funex
687. opabex
688. mptexg
689. mptexgf
690. mptex
691. mptexd
692. mptrabex
693. fex
694. fexd
695. mptfvmpt
696. eufnfv
697. funfvima
698. funfvima2
699. funfvima2d
700. fnfvima
701. fnfvimad
702. resfvresima
703. funfvima3
704. rexima
705. ralima
706. fvclss
707. elabrex
708. elabrexg
709. abrexco
710. imaiun
711. imauni
712. fniunfv
713. funiunfv
714. funiunfvf
715. eluniima
716. elunirn
717. elunirnALT
718. elunirn2OLD
719. fnunirn
720. dff13
721. dff13f
722. f1veqaeq
723. f1cofveqaeq
724. f1cofveqaeqALT
725. 2f1fvneq
726. f1mpt
727. f1fveq
728. f1elima
729. f1imass
730. f1imaeq
731. f1imapss
732. fpropnf1
733. f1dom3fv3dif
734. f1dom3el3dif
735. dff14a
736. dff14b
737. f12dfv
738. f13dfv
739. dff1o6
740. f1ocnvfv1
741. f1ocnvfv2
742. f1ocnvfv
743. f1ocnvfvb
744. nvof1o
745. nvocnv
746. f1cdmsn
747. fsnex
748. f1prex
749. f1ocnvdm
750. f1ocnvfvrneq
751. fcof1
752. fcofo
753. cbvfo
754. cbvexfo
755. cocan1
756. cocan2
757. fcof1oinvd
758. fcof1od
759. 2fcoidinvd
760. fcof1o
761. 2fvcoidd
762. 2fvidf1od
763. 2fvidinvd
764. foeqcnvco
765. f1eqcocnv
766. f1eqcocnvOLD
767. fveqf1o
768. nf1const
769. nf1oconst
770. f1ofvswap
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. imaeqsexv
827. 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. ovif
99. ovif2
100. ovif12
101. ifov
102. dmoprab
103. dmoprabss
104. rnoprab
105. rnoprab2
106. reldmoprab
107. oprabss
108. eloprabga
109. eloprabgaOLD
110. eloprabg
111. ssoprab2i
112. mpov
113. mpomptx
114. mpompt
115. mpodifsnif
116. mposnif
117. fconstmpo
118. resoprab
119. resoprab2
120. resmpo
121. funoprabg
122. funoprab
123. fnoprabg
124. mpofun
125. mpofunOLD
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. elrnmpores
139. ralrnmpo
140. rexrnmpo
141. ovid
142. ovidig
143. ovidi
144. ov
145. ovigg
146. ovig
147. ovmpt4g
148. ovmpos
149. ov2gf
150. ovmpodxf
151. ovmpodx
152. ovmpod
153. ovmpox
154. ovmpoga
155. ovmpoa
156. ovmpodf
157. ovmpodv
158. ovmpodv2
159. ovmpog
160. ovmpo
161. ovmpot
162. fvmpopr2d
163. ov3
164. ov6g
165. ovg
166. ovres
167. ovresd
168. oprres
169. oprssov
170. fovcdm
171. fovcdmda
172. fovcdmd
173. fnrnov
174. foov
175. fnovrn
176. ovelrn
177. funimassov
178. ovelimab
179. ovima0
180. ovconst2
181. oprssdm
182. nssdmovg
183. ndmovg
184. ndmov
185. ndmovcl
186. ndmovrcl
187. ndmovcom
188. ndmovass
189. ndmovdistr
190. ndmovord
191. ndmovordi
192. 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