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. axprlem3OLD
7. axprlem4OLD
8. axprlem5OLD
9. axprOLD
10. ax-pr
11. zfpair2
12. vsnex
13. snexg
14. snex
15. prex
16. exel
17. exexneq
18. exneq
19. dtru
20. el
21. sels
22. selsALT
23. elALT
24. dtruOLD
25. snelpwg
26. snelpwi
27. snelpwiOLD
28. snelpw
29. prelpw
30. prelpwi
31. rext
32. sspwb
33. unipw
34. univ
35. pwtr
36. ssextss
37. ssext
38. nssss
39. pweqb
40. intidg
41. intidOLD
42. moabex
43. rmorabex
44. euabex
45. nnullss
46. exss
47. opex
48. otex
49. elopg
50. elop
51. opi1
52. opi2
53. opeluu
54. op1stb
55. 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. copsex2dv
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. 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. friOLD
11. seex
12. exse
13. dffr2
14. dffr2ALT
15. frc
16. frss
17. sess1
18. sess2
19. freq1
20. freq2
21. freq12d
22. seeq1
23. seeq2
24. seeq12d
25. nffr
26. nfse
27. nfwe
28. frirr
29. fr2nr
30. fr0
31. frminex
32. efrirr
33. efrn2lp
34. epse
35. tz7.2
36. dfepfr
37. epfrc
38. wess
39. weeq1
40. weeq2
41. weeq12d
42. wefr
43. weso
44. wecmpep
45. wetrep
46. wefrc
47. we0
48. wereu
49. 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. elopaelxpOLD
95. bropaex12
96. opabssxp
97. brab2a
98. optocl
99. 2optocl
100. 3optocl
101. opbrop
102. 0xp
103. csbxp
104. releq
105. releqi
106. releqd
107. nfrel
108. sbcrel
109. relss
110. ssrel
111. ssrelOLD
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. difopabOLD
160. inxp
161. inxpOLD
162. xpindi
163. xpindir
164. xpiindi
165. xpriindi
166. eliunxp
167. opeliunxp2
168. raliunxp
169. rexiunxp
170. ralxp
171. rexxp
172. exopxfr
173. exopxfr2
174. djussxp
175. ralxpf
176. rexxpf
177. iunxpf
178. opabbi2dv
179. relop
180. ideqg
181. ideq
182. ididg
183. issetid
184. coss1
185. coss2
186. coeq1
187. coeq2
188. coeq1i
189. coeq2i
190. coeq1d
191. coeq2d
192. coeq12i
193. coeq12d
194. nfco
195. brcog
196. opelco2g
197. brcogw
198. eqbrrdva
199. brco
200. opelco
201. cnvss
202. cnveq
203. cnveqi
204. cnveqd
205. elcnv
206. elcnv2
207. nfcnv
208. brcnvg
209. opelcnvg
210. opelcnv
211. brcnv
212. csbcnv
213. csbcnvgALT
214. cnvco
215. cnvuni
216. dfdm3
217. dfrn2
218. dfrn3
219. elrn2g
220. elrng
221. elrn2
222. elrn
223. ssrelrn
224. dfdm4
225. dfdmf
226. csbdm
227. eldmg
228. eldm2g
229. eldm
230. eldm2
231. dmss
232. dmeq
233. dmeqi
234. dmeqd
235. opeldmd
236. opeldm
237. breldm
238. breldmg
239. dmun
240. dmin
241. breldmd
242. dmiun
243. dmuni
244. dmopab
245. dmopabelb
246. dmopab2rex
247. dmopabss
248. dmopab3
249. dm0
250. dmi
251. dmv
252. dmep
253. dm0rn0
254. rn0
255. rnep
256. reldm0
257. dmxp
258. dmxpOLD
259. dmxpid
260. dmxpin
261. xpid11
262. dmcnvcnv
263. rncnvcnv
264. elreldm
265. rneq
266. rneqi
267. rneqd
268. rnss
269. rnssi
270. brelrng
271. brelrn
272. opelrn
273. releldm
274. relelrn
275. releldmb
276. relelrnb
277. releldmi
278. relelrni
279. dfrnf
280. nfdm
281. nfrn
282. dmiin
283. rnopab
284. rnopabss
285. rnopab3
286. rnmpt
287. elrnmpt
288. elrnmpt1s
289. elrnmpt1
290. elrnmptg
291. elrnmpti
292. elrnmptd
293. elrnmpt1d
294. elrnmptdv
295. elrnmpt2d
296. dfiun3g
297. dfiin3g
298. dfiun3
299. dfiin3
300. riinint
301. relrn0
302. dmrnssfld
303. dmcoss
304. rncoss
305. dmcosseq
306. dmcosseqOLD
307. dmcoeq
308. rncoeq
309. reseq1
310. reseq2
311. reseq1i
312. reseq2i
313. reseq12i
314. reseq1d
315. reseq2d
316. reseq12d
317. nfres
318. csbres
319. res0
320. dfres3
321. opelres
322. brres
323. opelresi
324. brresi
325. opres
326. resieq
327. opelidres
328. resres
329. resundi
330. resundir
331. resindi
332. resindir
333. inres
334. resdifcom
335. resiun1
336. resiun2
337. resss
338. rescom
339. ssres
340. ssres2
341. relres
342. resabs1
343. resabs1i
344. resabs1d
345. resabs2
346. residm
347. dmresss
348. dmres
349. ssdmres
350. dmresexg
351. resima
352. resima2
353. rnresss
354. xpssres
355. elinxp
356. elres
357. elsnres
358. relssres
359. dmressnsn
360. eldmressnsn
361. eldmeldmressn
362. resdm
363. resexg
364. resexd
365. resex
366. resindm
367. resdmdfsn
368. reldisjun
369. relresdm1
370. resopab
371. iss
372. resopab2
373. resmpt
374. resmpt3
375. resmptf
376. resmptd
377. dfres2
378. mptss
379. elimampt
380. elidinxp
381. elidinxpid
382. elrid
383. idinxpres
384. idinxpresid
385. idssxp
386. opabresid
387. mptresid
388. dmresi
389. restidsing
390. iresn0n0
391. imaeq1
392. imaeq2
393. imaeq1i
394. imaeq2i
395. imaeq1d
396. imaeq2d
397. imaeq12d
398. dfima2
399. dfima3
400. elimag
401. elima
402. elima2
403. elima3
404. nfima
405. nfimad
406. imadmrn
407. imassrn
408. mptima
409. mptimass
410. imai
411. rnresi
412. resiima
413. ima0
414. 0ima
415. csbima12
416. imadisj
417. imadisjlnd
418. cnvimass
419. cnvimarndm
420. imasng
421. relimasn
422. elrelimasn
423. elimasng1
424. elimasn1
425. elimasng
426. elimasn
427. elimasni
428. args
429. elinisegg
430. eliniseg
431. epin
432. epini
433. iniseg
434. inisegn0
435. dffr3
436. dfse2
437. imass1
438. imass2
439. ndmima
440. relcnv
441. relbrcnvg
442. eliniseg2
443. relbrcnv
444. relco
445. cotrg
446. cotrgOLD
447. cotrgOLDOLD
448. cotr
449. idrefALT
450. cnvsym
451. cnvsymOLD
452. cnvsymOLDOLD
453. intasym
454. asymref
455. asymref2
456. intirr
457. brcodir
458. codir
459. qfto
460. xpidtr
461. trin2
462. poirr2
463. trinxp
464. soirri
465. sotri
466. son2lpi
467. sotri2
468. sotri3
469. poleloe
470. poltletr
471. somin1
472. somincom
473. somin2
474. soltmin
475. cnvopab
476. cnvopabOLD
477. mptcnv
478. cnv0
479. cnvi
480. cnvun
481. cnvdif
482. cnvin
483. rnun
484. rnin
485. rniun
486. rnuni
487. imaundi
488. imaundir
489. imadifssran
490. cnvimassrndm
491. dminss
492. imainss
493. inimass
494. inimasn
495. cnvxp
496. xp0
497. xpnz
498. xpeq0
499. xpdisj1
500. xpdisj2
501. xpsndisj
502. difxp
503. difxp1
504. difxp2
505. djudisj
506. xpdifid
507. resdisj
508. rnxp
509. dmxpss
510. rnxpss
511. rnxpid
512. ssxpb
513. xp11
514. xpcan
515. xpcan2
516. ssrnres
517. rninxp
518. dminxp
519. imainrect
520. xpima
521. xpima1
522. xpima2
523. xpimasn
524. sossfld
525. sofld
526. cnvcnv3
527. dfrel2
528. dfrel4v
529. dfrel4
530. cnvcnv
531. cnvcnv2
532. cnvcnvss
533. cnvrescnv
534. cnveqb
535. cnveq0
536. dfrel3
537. elid
538. dmresv
539. rnresv
540. dfrn4
541. csbrn
542. rescnvcnv
543. cnvcnvres
544. imacnvcnv
545. dmsnn0
546. rnsnn0
547. dmsn0
548. cnvsn0
549. dmsn0el
550. relsn2
551. dmsnopg
552. dmsnopss
553. dmpropg
554. dmsnop
555. dmprop
556. dmtpop
557. cnvcnvsn
558. dmsnsnsn
559. rnsnopg
560. rnpropg
561. cnvsng
562. rnsnop
563. op1sta
564. cnvsn
565. op2ndb
566. op2nda
567. opswap
568. cnvresima
569. resdm2
570. resdmres
571. resresdm
572. imadmres
573. resdmss
574. resdifdi
575. resdifdir
576. mptpreima
577. mptiniseg
578. dmmpt
579. dmmptss
580. dmmptg
581. rnmpt0f
582. rnmptn0
583. dfco2
584. dfco2a
585. coundi
586. coundir
587. cores
588. resco
589. imaco
590. rnco
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. relssdmrnOLD
608. resssxp
609. cnvssrndm
610. cossxp
611. relrelss
612. unielrel
613. relfld
614. relresfld
615. relcoi2
616. relcoi1
617. unidmrn
618. relcnvfld
619. dfdm2
620. unixp
621. unixp0
622. unixpid
623. ressn
624. cnviin
625. cnvpo
626. cnvso
627. xpco
628. xpcoid
629. elsnxp
630. reu3op
631. reuop
632. opreu2reurex
633. opreu2reu
634. dfpo2
635. csbcog
636. snres0
637. 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.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. 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. suceq
70. elsuci
71. elsucg
72. elsuc2g
73. elsuc
74. elsuc2
75. nfsuc
76. elelsuc
77. sucel
78. suc0
79. sucprc
80. unisucs
81. unisucg
82. unisuc
83. sssucid
84. sucidg
85. sucid
86. nsuceq0
87. eqelsuc
88. iunsuc
89. suctr
90. trsuc
91. trsucss
92. ordsssuc
93. onsssuc
94. ordsssuc2
95. onmindif
96. ordnbtwn
97. onnbtwn
98. sucssel
99. orddif
100. orduniss
101. ordtri2or
102. ordtri2or2
103. ordtri2or3
104. ordelinel
105. ordssun
106. ordequn
107. ordun
108. onunel
109. ordunisssuc
110. suc11
111. onun2
112. ontr
113. onunisuc
114. onordi
115. ontrciOLD
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. iotavalOLD
25. iotauni
26. iotaint
27. iota1
28. iotanul
29. iotassuniOLD
30. iotaexOLD
31. iota4
32. iota4an
33. iota5
34. iotabidv
35. iotabii
36. iotacl
37. iota2df
38. iota2d
39. iota2
40. iotan0
41. sniota
42. dfiota4
43. 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. f1imadifssran
99. funimaexg
100. funimaexgOLD
101. funimaex
102. isarep1
103. isarep1OLD
104. isarep2
105. fneq1
106. fneq2
107. fneq1d
108. fneq2d
109. fneq12d
110. fneq12
111. fneq1i
112. fneq2i
113. nffn
114. fnfun
115. fnfund
116. fnrel
117. fndm
118. fndmi
119. fndmd
120. funfni
121. fndmu
122. fnbr
123. fnop
124. fneu
125. fneu2
126. fnunres1
127. fnunres2
128. fnun
129. fnund
130. fnunop
131. fncofn
132. fnco
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. feq1dd
168. feq2d
169. feq3d
170. feq12d
171. feq123d
172. feq123
173. feq1i
174. feq2i
175. feq12i
176. feq23i
177. feq23d
178. nff
179. sbcfng
180. sbcfg
181. elimf
182. ffn
183. ffnd
184. dffn2
185. ffun
186. ffund
187. frel
188. freld
189. frn
190. frnd
191. fdm
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. fcod
208. fco2
209. fssxp
210. funssxp
211. ffdm
212. ffdmd
213. fdmrn
214. funcofd
215. opelf
216. fun
217. fun2
218. fun2d
219. fnfco
220. fssres
221. fssresd
222. fssres2
223. fresin
224. resasplit
225. fresaun
226. fresaunres2
227. fresaunres1
228. fcoi1
229. fcoi2
230. feu
231. fcnvres
232. fimacnvdisj
233. fint
234. fin
235. f0
236. f00
237. f0bi
238. f0dom0
239. f0rn0
240. fconst
241. fconstg
242. fnconstg
243. fconst6g
244. fconst6
245. f1eq1
246. f1eq2
247. f1eq3
248. nff1
249. dff12
250. f1f
251. f1fn
252. f1fun
253. f1rel
254. f1dm
255. f1ss
256. f1ssr
257. f1ssres
258. f1resf1
259. f1cnvcnv
260. f1cof1
261. f1co
262. foeq1
263. foeq2
264. foeq3
265. nffo
266. fof
267. fofun
268. fofn
269. forn
270. dffo2
271. foima
272. dffn4
273. funforn
274. fodmrnu
275. fimadmfo
276. fores
277. fimadmfoALT
278. focnvimacdmdm
279. focofo
280. foco
281. foconst
282. f1oeq1
283. f1oeq2
284. f1oeq3
285. f1oeq23
286. f1eq123d
287. foeq123d
288. f1oeq123d
289. f1oeq1d
290. f1oeq2d
291. f1oeq3d
292. nff1o
293. f1of1
294. f1of
295. f1ofn
296. f1ofun
297. f1orel
298. f1odm
299. dff1o2
300. dff1o3
301. f1ofo
302. dff1o4
303. dff1o5
304. f1orn
305. f1f1orn
306. f1ocnv
307. f1ocnvb
308. f1ores
309. f1orescnv
310. f1imacnv
311. foimacnv
312. foun
313. f1oun
314. f1un
315. resdif
316. resin
317. f1oco
318. f1cnv
319. funcocnv2
320. fococnv2
321. f1ococnv2
322. f1cocnv2
323. f1ococnv1
324. f1cocnv1
325. funcoeqres
326. f1ssf1
327. f10
328. f10d
329. f1o00
330. fo00
331. f1o0
332. f1oi
333. f1ovi
334. f1osn
335. f1osng
336. f1sng
337. fsnd
338. f1oprswap
339. f1oprg
340. tz6.12-2
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-1OLD
377. tz6.12
378. tz6.12f
379. tz6.12cOLD
380. tz6.12i
381. fvbr0
382. fvrn0
383. fvn0fvelrn
384. elfvunirn
385. fvssunirn
386. fvssunirnOLD
387. ndmfv
388. ndmfvrcl
389. elfvdm
390. elfvex
391. elfvexd
392. eliman0
393. nfvres
394. nfunsn
395. fvfundmfvn0
396. 0fv
397. fv2prc
398. elfv2ex
399. fveqres
400. csbfv12
401. csbfv2g
402. csbfv
403. funbrfv
404. funopfv
405. fnbrfvb
406. fnopfvb
407. fvelima2
408. funbrfvb
409. funopfvb
410. fnbrfvb2
411. fdmeu
412. funbrfv2b
413. dffn5
414. fnrnfv
415. fvelrnb
416. foelcdmi
417. dfimafn
418. dfimafn2
419. funimass4
420. fvelima
421. funimassd
422. fvelimad
423. feqmptd
424. feqresmpt
425. feqmptdf
426. dffn5f
427. fvelimab
428. fvelimabd
429. fimarab
430. unima
431. fvi
432. fviss
433. fniinfv
434. fnsnfv
435. opabiotafun
436. opabiotadm
437. opabiota
438. fnimapr
439. fnimatpd
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. fvmptd4
487. fvmptn
488. fvmptss2
489. elfvmptrab1w
490. elfvmptrab1
491. elfvmptrab
492. fvopab4ndm
493. fvmptndm
494. fvmptrabfv
495. fvopab5
496. fvopab6
497. eqfnfv
498. eqfnfv2
499. eqfnfv3
500. eqfnfvd
501. eqfnfv2f
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. iinpreima
536. intpreima
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. feldmfvelcdm
553. rexrn
554. ralrn
555. elrnrexdm
556. elrnrexdmb
557. eldmrexrn
558. eldmrexrnb
559. fvcofneq
560. ralrnmptw
561. rexrnmptw
562. ralrnmpt
563. rexrnmpt
564. f0cli
565. dff2
566. dff3
567. dff4
568. dffo3
569. dffo4
570. dffo5
571. exfo
572. dffo3f
573. foelrn
574. foelrnf
575. foco2
576. fmpt
577. f1ompt
578. fmpti
579. fvmptelcdm
580. fmptd
581. fmpttd
582. fmpt3d
583. fmptdf
584. fompt
585. ffnfv
586. ffnfvf
587. fnfvrnss
588. fcdmssb
589. rnmptss
590. fmpt2d
591. ffvresb
592. fssrescdmd
593. f1oresrab
594. f1ossf1o
595. fmptco
596. fmptcof
597. fmptcos
598. cofmpt
599. fcompt
600. fcoconst
601. fsn
602. fsn2
603. fsng
604. fsn2g
605. xpsng
606. xpprsng
607. xpsn
608. f1o2sn
609. residpr
610. dfmpt
611. fnasrn
612. idref
613. funiun
614. funopsn
615. funop
616. funopdmsn
617. funsndifnop
618. funsneqopb
619. ressnop0
620. fpr
621. fprg
622. ftpg
623. ftp
624. fnressn
625. funressn
626. fressnfv
627. fvrnressn
628. fvressn
629. fvn0fvelrnOLD
630. fvconst
631. fnsnr
632. fnsnbg
633. fnsnb
634. fnsnbOLD
635. fmptsn
636. fmptsng
637. fmptsnd
638. fmptap
639. fmptapd
640. fmptpr
641. fvresi
642. fninfp
643. fnelfp
644. fndifnfp
645. fnelnfp
646. fnnfpeq0
647. fvunsn
648. fvsng
649. fvsn
650. fvsnun1
651. fvsnun2
652. fnsnsplit
653. fsnunf
654. fsnunf2
655. fsnunfv
656. fsnunres
657. funresdfunsn
658. fvpr1g
659. fvpr2g
660. fvpr1
661. fvpr2
662. fprb
663. fvtp1
664. fvtp2
665. fvtp3
666. fvtp1g
667. fvtp2g
668. fvtp3g
669. tpres
670. fvconst2g
671. fconst2g
672. fvconst2
673. fconst2
674. fconst5
675. rnmptc
676. fnprb
677. fntpb
678. fnpr2g
679. fpr2g
680. fconstfv
681. fconst3
682. fconst4
683. resfunexg
684. resiexd
685. fnex
686. fnexd
687. funex
688. opabex
689. mptexg
690. mptexgf
691. mptex
692. mptexd
693. mptrabex
694. fex
695. fexd
696. mptfvmpt
697. eufnfv
698. funfvima
699. funfvima2
700. funfvima2d
701. fnfvima
702. fnfvimad
703. resfvresima
704. funfvima3
705. ralima
706. rexima
707. reximaOLD
708. ralimaOLD
709. fvclss
710. elabrex
711. elabrexg
712. abrexco
713. imaiun
714. imauni
715. fniunfv
716. funiunfv
717. funiunfvf
718. eluniima
719. elunirn
720. elunirnALT
721. elunirn2OLD
722. fnunirn
723. dff13
724. dff13f
725. f1veqaeq
726. f1cofveqaeq
727. f1cofveqaeqALT
728. dff14i
729. 2f1fvneq
730. f1mpt
731. f1fveq
732. f1elima
733. f1imass
734. f1imaeq
735. f1imapss
736. fpropnf1
737. f1dom3fv3dif
738. f1dom3el3dif
739. dff14a
740. dff14b
741. f1ounsn
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. fveqf1o
772. f1ocoima
773. nf1const
774. nf1oconst
775. f1ofvswap
776. fvf1pr
777. fliftrel
778. fliftel
779. fliftel1
780. fliftcnv
781. fliftfun
782. fliftfund
783. fliftfuns
784. fliftf
785. fliftval
786. isoeq1
787. isoeq2
788. isoeq3
789. isoeq4
790. isoeq5
791. nfiso
792. isof1o
793. isof1oidb
794. isof1oopb
795. isorel
796. soisores
797. soisoi
798. isoid
799. isocnv
800. isocnv2
801. isocnv3
802. isores2
803. isores1
804. isores3
805. isotr
806. isomin
807. isoini
808. isoini2
809. isofrlem
810. isoselem
811. isofr
812. isose
813. isofr2
814. isopolem
815. isopo
816. isosolem
817. isoso
818. isowe
819. isowe2
820. f1oiso
821. f1oiso2
822. f1owe
823. weniso
824. weisoeq
825. weisoeq2
826. knatar
827. fvresval
828. funeldmb
829. eqfunresadj
830. eqfunressuc
831. fnssintima
832. imaeqsexvOLD
833. imaeqsalvOLD
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. opabresex2d
57. fvmptopab
58. fvmptopabOLD
59. f1opr
60. brfvopab
61. dfoprab2
62. reloprab
63. oprabv
64. nfoprab1
65. nfoprab2
66. nfoprab3
67. nfoprab
68. oprabbid
69. oprabbidv
70. oprabbii
71. ssoprab2
72. ssoprab2b
73. eqoprab2bw
74. eqoprab2b
75. mpoeq123
76. mpoeq12
77. mpoeq123dva
78. mpoeq123dv
79. mpoeq123i
80. mpoeq3dva
81. mpoeq3ia
82. mpoeq3dv
83. nfmpo1
84. nfmpo2
85. nfmpo
86. 0mpo0
87. mpo0v
88. mpo0
89. oprab4
90. cbvoprab1
91. cbvoprab2
92. cbvoprab12
93. cbvoprab12v
94. cbvoprab3
95. cbvoprab3v
96. cbvmpox
97. cbvmpo
98. cbvmpov
99. elimdelov
100. brif1
101. ovif
102. ovif2
103. ovif12
104. ifov
105. ifmpt2v
106. dmoprab
107. dmoprabss
108. rnoprab
109. rnoprab2
110. reldmoprab
111. oprabss
112. eloprabga
113. eloprabg
114. ssoprab2i
115. mpov
116. mpomptx
117. mpompt
118. mpodifsnif
119. mposnif
120. fconstmpo
121. resoprab
122. resoprab2
123. resmpo
124. funoprabg
125. funoprab
126. fnoprabg
127. mpofun
128. fnoprab
129. ffnov
130. fovcld
131. fovcl
132. eqfnov
133. eqfnov2
134. fnov
135. mpo2eqb
136. rnmpo
137. reldmmpo
138. elrnmpog
139. elrnmpo
140. elimampo
141. elrnmpores
142. ralrnmpo
143. rexrnmpo
144. ovid
145. ovidig
146. ovidi
147. ov
148. ovigg
149. ovig
150. ovmpt4g
151. ovmpos
152. ov2gf
153. ovmpodxf
154. ovmpodx
155. ovmpod
156. ovmpox
157. ovmpoga
158. ovmpoa
159. ovmpodf
160. ovmpodv
161. ovmpodv2
162. ovmpog
163. ovmpo
164. ovmpot
165. fvmpopr2d
166. ov3
167. ov6g
168. ovg
169. ovres
170. ovresd
171. oprres
172. oprssov
173. fovcdm
174. fovcdmda
175. fovcdmd
176. fnrnov
177. foov
178. fnovrn
179. ovelrn
180. funimassov
181. ovelimab
182. ovima0
183. ovconst2
184. oprssdm
185. nssdmovg
186. ndmovg
187. ndmov
188. ndmovcl
189. ndmovrcl
190. ndmovcom
191. ndmovass
192. ndmovdistr
193. ndmovord
194. ndmovordi
195. 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