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