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. snelpwg
25. snelpwi
26. snelpw
27. prelpw
28. prelpwi
29. rext
30. sspwb
31. unipw
32. univ
33. pwtr
34. ssextss
35. ssext
36. nssss
37. pweqb
38. intidg
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. 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. elopabr
38. elopabran
39. rbropapd
40. rbropap
41. 2rbropap
42. 0nelopab
43. brabv
Power class of union and intersection
1. pwin
2. pwssun
3. pwun
The identity relation
1. cid
2. df-id
3. dfid4
4. dfid2
5. dfid3
The membership relation (or epsilon relation)
1. cep
2. df-eprel
3. epelg
4. epeli
5. epel
6. 0sn0ep
7. epn0
Partial and total orderings
1. wpo
2. wor
3. df-po
4. df-so
5. poss
6. poeq1
7. poeq2
8. poeq12d
9. nfpo
10. nfso
11. pocl
12. ispod
13. swopolem
14. swopo
15. poirr
16. potr
17. po2nr
18. po3nr
19. po2ne
20. po0
21. pofun
22. sopo
23. soss
24. soeq1
25. soeq2
26. soeq12d
27. sonr
28. sotr
29. sotrd
30. solin
31. so2nr
32. so3nr
33. sotric
34. sotrieq
35. sotrieq2
36. soasym
37. sotr2
38. issod
39. issoi
40. isso2i
41. so0
42. somo
43. sotrine
44. sotr3
Founded and well-ordering relations
1. wfr
2. wse
3. wwe
4. df-fr
5. df-se
6. df-we
7. dffr6
8. frd
9. fri
10. seex
11. exse
12. dffr2
13. dffr2ALT
14. frc
15. frss
16. sess1
17. sess2
18. freq1
19. freq2
20. freq12d
21. seeq1
22. seeq2
23. seeq12d
24. nffr
25. nfse
26. nfwe
27. frirr
28. fr2nr
29. fr0
30. frminex
31. efrirr
32. efrn2lp
33. epse
34. tz7.2
35. dfepfr
36. epfrc
37. wess
38. weeq1
39. weeq2
40. weeq12d
41. wefr
42. weso
43. wecmpep
44. wetrep
45. wefrc
46. we0
47. wereu
48. wereu2
Relations
1. cxp
2. ccnv
3. cdm
4. crn
5. cres
6. cima
7. ccom
8. wrel
9. df-xp
10. df-rel
11. df-cnv
12. df-co
13. df-dm
14. df-rn
15. df-res
16. df-ima
17. xpeq1
18. xpss12
19. xpss
20. inxpssres
21. relxp
22. xpss1
23. xpss2
24. xpeq2
25. elxpi
26. elxp
27. elxp2
28. xpeq12
29. xpeq1i
30. xpeq2i
31. xpeq12i
32. xpeq1d
33. xpeq2d
34. xpeq12d
35. sqxpeqd
36. nfxp
37. 0nelxp
38. 0nelelxp
39. opelxp
40. opelxpi
41. opelxpii
42. opelxpd
43. opelvv
44. opelvvg
45. opelxp1
46. opelxp2
47. otelxp
48. otelxp1
49. otel3xp
50. opabssxpd
51. rabxp
52. brxp
53. pwvrel
54. pwvabrel
55. brrelex12
56. brrelex1
57. brrelex2
58. brrelex12i
59. brrelex1i
60. brrelex2i
61. nprrel12
62. nprrel
63. 0nelrel0
64. 0nelrel
65. fconstmpt
66. vtoclr
67. opthprc
68. brel
69. elxp3
70. opeliunxp
71. opeliun2xp
72. xpundi
73. xpundir
74. xpiundi
75. xpiundir
76. iunxpconst
77. xpun
78. elvv
79. elvvv
80. elvvuni
81. brinxp2
82. brinxp
83. opelinxp
84. poinxp
85. soinxp
86. frinxp
87. seinxp
88. weinxp
89. posn
90. sosn
91. frsn
92. wesn
93. elopaelxp
94. bropaex12
95. opabssxp
96. brab2a
97. optocl
98. optoclOLD
99. 2optocl
100. 3optocl
101. opbrop
102. 0xp
103. csbxp
104. releq
105. releqi
106. releqd
107. nfrel
108. sbcrel
109. relss
110. ssrel
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. inxp
159. inxpOLD
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. rnopabss
282. rnopab3
283. rnmpt
284. elrnmpt
285. elrnmpt1s
286. elrnmpt1
287. elrnmptg
288. elrnmpti
289. elrnmptd
290. elrnmpt1d
291. elrnmptdv
292. elrnmpt2d
293. dfiun3g
294. dfiin3g
295. dfiun3
296. dfiin3
297. riinint
298. relrn0
299. dmrnssfld
300. dmcoss
301. dmcossOLD
302. rncoss
303. dmcosseq
304. dmcosseqOLD
305. dmcosseqOLDOLD
306. dmcoeq
307. rncoeq
308. reseq1
309. reseq2
310. reseq1i
311. reseq2i
312. reseq12i
313. reseq1d
314. reseq2d
315. reseq12d
316. nfres
317. csbres
318. res0
319. dfres3
320. opelres
321. brres
322. opelresi
323. brresi
324. opres
325. resieq
326. opelidres
327. resres
328. resundi
329. resundir
330. resindi
331. resindir
332. inres
333. resdifcom
334. resiun1
335. resiun2
336. resss
337. rescom
338. ssres
339. ssres2
340. relres
341. resabs1
342. resabs1i
343. resabs1d
344. resabs2
345. residm
346. dmresss
347. dmres
348. ssdmres
349. dmresexg
350. resima
351. resima2
352. rnresss
353. xpssres
354. elinxp
355. elres
356. elsnres
357. relssres
358. dmressnsn
359. eldmressnsn
360. eldmeldmressn
361. resdm
362. resexg
363. resexd
364. resex
365. resindm
366. resdmdfsn
367. reldisjun
368. relresdm1
369. resopab
370. iss
371. resopab2
372. resmpt
373. resmpt3
374. resmptf
375. resmptd
376. dfres2
377. mptss
378. elimampt
379. elidinxp
380. elidinxpid
381. elrid
382. idinxpres
383. idinxpresid
384. idssxp
385. opabresid
386. mptresid
387. dmresi
388. restidsing
389. iresn0n0
390. imaeq1
391. imaeq2
392. imaeq1i
393. imaeq2i
394. imaeq1d
395. imaeq2d
396. imaeq12d
397. dfima2
398. dfima3
399. elimag
400. elima
401. elima2
402. elima3
403. nfima
404. nfimad
405. imadmrn
406. imassrn
407. mptima
408. mptimass
409. imai
410. rnresi
411. resiima
412. ima0
413. 0ima
414. csbima12
415. imadisj
416. imadisjlnd
417. cnvimass
418. cnvimarndm
419. imasng
420. relimasn
421. elrelimasn
422. elimasng1
423. elimasn1
424. elimasng
425. elimasn
426. elimasni
427. args
428. elinisegg
429. eliniseg
430. epin
431. epini
432. iniseg
433. inisegn0
434. dffr3
435. dfse2
436. imass1
437. imass2
438. ndmima
439. relcnv
440. relbrcnvg
441. eliniseg2
442. relbrcnv
443. relco
444. cotrg
445. cotr
446. idrefALT
447. cnvsym
448. intasym
449. asymref
450. asymref2
451. intirr
452. brcodir
453. codir
454. qfto
455. xpidtr
456. trin2
457. poirr2
458. trinxp
459. soirri
460. sotri
461. son2lpi
462. sotri2
463. sotri3
464. poleloe
465. poltletr
466. somin1
467. somincom
468. somin2
469. soltmin
470. cnvopab
471. cnvopabOLD
472. mptcnv
473. cnv0
474. cnvi
475. cnvun
476. cnvdif
477. cnvin
478. rnun
479. rnin
480. rniun
481. rnuni
482. imaundi
483. imaundir
484. imadifssran
485. cnvimassrndm
486. dminss
487. imainss
488. inimass
489. inimasn
490. cnvxp
491. xp0
492. xpnz
493. xpeq0
494. xpdisj1
495. xpdisj2
496. xpsndisj
497. difxp
498. difxp1
499. difxp2
500. djudisj
501. xpdifid
502. resdisj
503. rnxp
504. dmxpss
505. rnxpss
506. rnxpid
507. ssxpb
508. xp11
509. xpcan
510. xpcan2
511. ssrnres
512. rninxp
513. dminxp
514. imainrect
515. xpima
516. xpima1
517. xpima2
518. xpimasn
519. sossfld
520. sofld
521. cnvcnv3
522. dfrel2
523. dfrel4v
524. dfrel4
525. cnvcnv
526. cnvcnv2
527. cnvcnvss
528. cnvrescnv
529. cnveqb
530. cnveq0
531. dfrel3
532. elid
533. dmresv
534. rnresv
535. dfrn4
536. csbrn
537. rescnvcnv
538. cnvcnvres
539. imacnvcnv
540. dmsnn0
541. rnsnn0
542. dmsn0
543. cnvsn0
544. dmsn0el
545. relsn2
546. dmsnopg
547. dmsnopss
548. dmpropg
549. dmsnop
550. dmprop
551. dmtpop
552. cnvcnvsn
553. dmsnsnsn
554. rnsnopg
555. rnpropg
556. cnvsng
557. rnsnop
558. op1sta
559. cnvsn
560. op2ndb
561. op2nda
562. opswap
563. cnvresima
564. resdm2
565. resdmres
566. resresdm
567. imadmres
568. resdmss
569. resdifdi
570. resdifdir
571. mptpreima
572. mptiniseg
573. dmmpt
574. dmmptss
575. dmmptg
576. rnmpt0f
577. rnmptn0
578. dfco2
579. dfco2a
580. coundi
581. coundir
582. cores
583. resco
584. imaco
585. rnco
586. rnco2
587. dmco
588. coeq0
589. coiun
590. cocnvcnv1
591. cocnvcnv2
592. cores2
593. co02
594. co01
595. coi1
596. coi2
597. coires1
598. coass
599. relcnvtrg
600. relcnvtr
601. relssdmrn
602. resssxp
603. cnvssrndm
604. cossxp
605. relrelss
606. unielrel
607. relfld
608. relresfld
609. relcoi2
610. relcoi1
611. unidmrn
612. relcnvfld
613. dfdm2
614. unixp
615. unixp0
616. unixpid
617. ressn
618. cnviin
619. cnvpo
620. cnvso
621. xpco
622. xpcoid
623. elsnxp
624. reu3op
625. reuop
626. opreu2reurex
627. opreu2reu
628. dfpo2
629. csbcog
630. snres0
631. imaindm
The Predecessor Class
1. cpred
2. df-pred
3. predeq123
4. predeq1
5. predeq2
6. predeq3
7. nfpred
8. csbpredg
9. predpredss
10. predss
11. sspred
12. dfpred2
13. dfpred3
14. dfpred3g
15. elpredgg
16. elpredg
17. elpredimg
18. elpredim
19. elpred
20. predexg
21. dffr4
22. predel
23. predtrss
24. predpo
25. predso
26. setlikespec
27. predidm
28. predin
29. predun
30. preddif
31. predep
32. trpred
33. preddowncl
34. predpoirr
35. predfrirr
36. pred0
37. dfse3
38. predrelss
39. predprc
40. predres
Well-founded induction (variant)
1. frpomin
2. frpomin2
3. frpoind
4. frpoinsg
5. frpoins2fg
6. frpoins2g
7. frpoins3g
Well-ordered induction
1. tz6.26
2. tz6.26i
3. wfi
4. wfii
5. wfisg
6. wfis
7. wfis2fg
8. wfis2f
9. wfis2g
10. wfis2
11. wfis3
Ordinals
1. word
2. con0
3. wlim
4. csuc
5. df-ord
6. df-on
7. df-lim
8. df-suc
9. ordeq
10. elong
11. elon
12. eloni
13. elon2
14. limeq
15. ordwe
16. ordtr
17. ordfr
18. ordelss
19. trssord
20. ordirr
21. nordeq
22. ordn2lp
23. tz7.5
24. ordelord
25. tron
26. ordelon
27. onelon
28. tz7.7
29. ordelssne
30. ordelpss
31. ordsseleq
32. ordin
33. onin
34. ordtri3or
35. ordtri1
36. ontri1
37. ordtri2
38. ordtri3
39. ordtri4
40. orddisj
41. onfr
42. onelpss
43. onsseleq
44. onelss
45. oneltri
46. ordtr1
47. ordtr2
48. ordtr3
49. ontr1
50. ontr2
51. onelssex
52. ordunidif
53. ordintdif
54. onintss
55. oneqmini
56. ord0
57. 0elon
58. ord0eln0
59. on0eln0
60. dflim2
61. inton
62. nlim0
63. limord
64. limuni
65. limuni2
66. 0ellim
67. limelon
68. onn0
69. suceqd
70. suceq
71. elsuci
72. elsucg
73. elsuc2g
74. elsuc
75. elsuc2
76. nfsuc
77. elelsuc
78. sucel
79. suc0
80. sucprc
81. unisucs
82. unisucg
83. unisuc
84. sssucid
85. sucidg
86. sucid
87. nsuceq0
88. eqelsuc
89. iunsuc
90. suctr
91. trsuc
92. trsucss
93. ordsssuc
94. onsssuc
95. ordsssuc2
96. onmindif
97. ordnbtwn
98. onnbtwn
99. sucssel
100. orddif
101. orduniss
102. ordtri2or
103. ordtri2or2
104. ordtri2or3
105. ordelinel
106. ordssun
107. ordequn
108. ordun
109. onunel
110. ordunisssuc
111. suc11
112. onun2
113. ontr
114. onunisuc
115. onordi
116. onirri
117. oneli
118. onelssi
119. onssneli
120. onssnel2i
121. onelini
122. oneluni
123. onunisuci
124. onsseli
125. onun2i
126. unizlim
127. on0eqel
128. snsn0non
129. onxpdisj
130. onnev
Definite description binder (inverted iota)
1. cio
2. iotajust
3. df-iota
4. dfiota2
5. nfiota1
6. nfiotadw
7. nfiotaw
8. nfiotad
9. nfiota
10. cbviotaw
11. cbviotavw
12. cbviota
13. cbviotav
14. sb8iota
15. iotaeq
16. iotabi
17. uniabio
18. iotaval2
19. iotauni2
20. iotanul2
21. iotaval
22. iotassuni
23. iotaex
24. iotauni
25. iotaint
26. iota1
27. iotanul
28. iota4
29. iota4an
30. iota5
31. iotabidv
32. iotabii
33. iotacl
34. iota2df
35. iota2d
36. iota2
37. iotan0
38. sniota
39. dfiota4
40. csbiota
Functions
1. wfun
2. wfn
3. wf
4. wf1
5. wfo
6. wf1o
7. cfv
8. wiso
9. df-fun
10. df-fn
11. df-f
12. df-f1
13. df-fo
14. df-f1o
15. df-fv
16. df-isom
17. dffun2
18. dffun6
19. dffun3
20. dffun4
21. dffun5
22. dffun6f
23. funmo
24. funrel
25. 0nelfun
26. funss
27. funeq
28. funeqi
29. funeqd
30. nffun
31. sbcfung
32. funeu
33. funeu2
34. dffun7
35. dffun8
36. dffun9
37. funfn
38. funfnd
39. funi
40. nfunv
41. funopg
42. funopab
43. funopabeq
44. funopab4
45. funmpt
46. funmpt2
47. funco
48. funresfunco
49. funres
50. funresd
51. funssres
52. fun2ssres
53. funun
54. fununmo
55. fununfun
56. fundif
57. funcnvsn
58. funsng
59. fnsng
60. funsn
61. funprg
62. funtpg
63. funpr
64. funtp
65. fnsn
66. fnprg
67. fntpg
68. fntp
69. funcnvpr
70. funcnvtp
71. funcnvqp
72. fun0
73. funcnv0
74. funcnvcnv
75. funcnv2
76. funcnv
77. funcnv3
78. fun2cnv
79. svrelfun
80. fncnv
81. fun11
82. fununi
83. funin
84. funres11
85. funcnvres
86. cnvresid
87. funcnvres2
88. funimacnv
89. funimass1
90. funimass2
91. imadif
92. imain
93. f1imadifssran
94. funimaexg
95. funimaex
96. isarep1
97. isarep2
98. fneq1
99. fneq2
100. fneq1d
101. fneq2d
102. fneq12d
103. fneq12
104. fneq1i
105. fneq2i
106. nffn
107. fnfun
108. fnfund
109. fnrel
110. fndm
111. fndmi
112. fndmd
113. funfni
114. fndmu
115. fnbr
116. fnop
117. fneu
118. fneu2
119. fnunres1
120. fnunres2
121. fnun
122. fnund
123. fnunop
124. fncofn
125. fnco
126. fnresdm
127. fnresdisj
128. 2elresin
129. fnssresb
130. fnssres
131. fnssresd
132. fnresin1
133. fnresin2
134. fnres
135. idfn
136. fnresi
137. fnima
138. fn0
139. fnimadisj
140. fnimaeq0
141. dfmpt3
142. mptfnf
143. fnmptf
144. fnopabg
145. fnopab
146. mptfng
147. fnmpt
148. fnmptd
149. mpt0
150. fnmpti
151. dmmpti
152. dmmptd
153. mptun
154. partfun
155. feq1
156. feq2
157. feq3
158. feq23
159. feq1d
160. feq1dd
161. feq2d
162. feq3d
163. feq2dd
164. feq3dd
165. feq12d
166. feq123d
167. feq123
168. feq1i
169. feq2i
170. feq12i
171. feq23i
172. feq23d
173. nff
174. sbcfng
175. sbcfg
176. elimf
177. ffn
178. ffnd
179. dffn2
180. ffun
181. ffund
182. frel
183. freld
184. frn
185. frnd
186. fdm
187. fdmd
188. fdmi
189. dffn3
190. ffrn
191. ffrnb
192. ffrnbd
193. fss
194. fssd
195. fssdmd
196. fssdm
197. fimass
198. fimassd
199. fimacnv
200. fcof
201. fco
202. fcod
203. fco2
204. fssxp
205. funssxp
206. ffdm
207. ffdmd
208. fdmrn
209. funcofd
210. opelf
211. fun
212. fun2
213. fun2d
214. fnfco
215. fssres
216. fssresd
217. fssres2
218. fresin
219. resasplit
220. fresaun
221. fresaunres2
222. fresaunres1
223. fcoi1
224. fcoi2
225. feu
226. fcnvres
227. fimacnvdisj
228. fint
229. fin
230. f0
231. f00
232. f0bi
233. f0dom0
234. f0rn0
235. fconst
236. fconstg
237. fnconstg
238. fconst6g
239. fconst6
240. f1eq1
241. f1eq2
242. f1eq3
243. nff1
244. dff12
245. f1f
246. f1fn
247. f1fun
248. f1rel
249. f1dm
250. f1ss
251. f1ssr
252. f1ssres
253. f1resf1
254. f1cnvcnv
255. f1cof1
256. f1co
257. foeq1
258. foeq2
259. foeq3
260. nffo
261. fof
262. fofun
263. fofn
264. forn
265. dffo2
266. foima
267. dffn4
268. funforn
269. fodmrnu
270. fimadmfo
271. fores
272. fimadmfoALT
273. focnvimacdmdm
274. focofo
275. foco
276. foconst
277. f1oeq1
278. f1oeq2
279. f1oeq3
280. f1oeq23
281. f1eq123d
282. foeq123d
283. f1oeq123d
284. f1oeq1d
285. f1oeq2d
286. f1oeq3d
287. nff1o
288. f1of1
289. f1of
290. f1ofn
291. f1ofun
292. f1orel
293. f1odm
294. dff1o2
295. dff1o3
296. f1ofo
297. dff1o4
298. dff1o5
299. f1orn
300. f1f1orn
301. f1ocnv
302. f1ocnvb
303. f1ores
304. f1orescnv
305. f1imacnv
306. foimacnv
307. foun
308. f1oun
309. f1un
310. resdif
311. resin
312. f1oco
313. f1cnv
314. funcocnv2
315. fococnv2
316. f1ococnv2
317. f1cocnv2
318. f1ococnv1
319. f1cocnv1
320. funcoeqres
321. f1ssf1
322. f10
323. f10d
324. f1o00
325. fo00
326. f1o0
327. f1oi
328. f1ovi
329. f1osn
330. f1osng
331. f1sng
332. fsnd
333. f1oprswap
334. f1oprg
335. tz6.12-2
336. fveu
337. brprcneu
338. brprcneuALT
339. fvprc
340. fvprcALT
341. rnfvprc
342. fv2
343. dffv3
344. dffv4
345. elfv
346. fveq1
347. fveq2
348. fveq1i
349. fveq1d
350. fveq2i
351. fveq2d
352. 2fveq3
353. fveq12i
354. fveq12d
355. fveqeq2d
356. fveqeq2
357. nffv
358. nffvmpt1
359. nffvd
360. fvex
361. fvexi
362. fvexd
363. fvif
364. iffv
365. fv3
366. fvres
367. fvresd
368. funssfv
369. tz6.12c
370. tz6.12-1
371. tz6.12
372. tz6.12f
373. tz6.12i
374. fvbr0
375. fvrn0
376. fvn0fvelrn
377. elfvunirn
378. fvssunirn
379. ndmfv
380. ndmfvrcl
381. elfvdm
382. elfvex
383. elfvexd
384. eliman0
385. nfvres
386. nfunsn
387. fvfundmfvn0
388. 0fv
389. fv2prc
390. elfv2ex
391. fveqres
392. csbfv12
393. csbfv2g
394. csbfv
395. funbrfv
396. funopfv
397. fnbrfvb
398. fnopfvb
399. fvelima2
400. funbrfvb
401. funopfvb
402. fnbrfvb2
403. fdmeu
404. funbrfv2b
405. dffn5
406. fnrnfv
407. fvelrnb
408. foelcdmi
409. dfimafn
410. dfimafn2
411. funimass4
412. fvelima
413. funimassd
414. fvelimad
415. feqmptd
416. feqresmpt
417. feqmptdf
418. dffn5f
419. fvelimab
420. fvelimabd
421. fimarab
422. unima
423. fvi
424. fviss
425. fniinfv
426. fnsnfv
427. opabiotafun
428. opabiotadm
429. opabiota
430. fnimapr
431. fnimatpd
432. ssimaex
433. ssimaexg
434. funfv
435. funfv2
436. funfv2f
437. fvun
438. fvun1
439. fvun2
440. fvun1d
441. fvun2d
442. dffv2
443. dmfco
444. fvco2
445. fvco
446. fvco3
447. fvco3d
448. fvco4i
449. fvopab3g
450. fvopab3ig
451. brfvopabrbr
452. fvmptg
453. fvmpti
454. fvmpt
455. fvmpt2f
456. fvtresfn
457. fvmpts
458. fvmpt3
459. fvmpt3i
460. fvmptdf
461. fvmptd
462. fvmptd2
463. mptrcl
464. fvmpt2i
465. fvmpt2
466. fvmptss
467. fvmpt2d
468. fvmptex
469. fvmptd3f
470. fvmptd2f
471. fvmptdv
472. fvmptdv2
473. mpteqb
474. fvmptt
475. fvmptf
476. fvmptnf
477. fvmptd3
478. fvmptd4
479. fvmptn
480. fvmptss2
481. elfvmptrab1w
482. elfvmptrab1
483. elfvmptrab
484. fvopab4ndm
485. fvmptndm
486. fvmptrabfv
487. fvopab5
488. fvopab6
489. eqfnfv
490. eqfnfv2
491. eqfnfv3
492. eqfnfvd
493. eqfnfv2f
494. eqfunfv
495. eqfnun
496. fvreseq0
497. fvreseq1
498. fvreseq
499. fnmptfvd
500. fndmdif
501. fndmdifcom
502. fndmdifeq0
503. fndmin
504. fneqeql
505. fneqeql2
506. fnreseql
507. chfnrn
508. funfvop
509. funfvbrb
510. fvimacnvi
511. fvimacnv
512. funimass3
513. funimass5
514. funconstss
515. fvimacnvALT
516. elpreima
517. elpreimad
518. fniniseg
519. fncnvima2
520. fniniseg2
521. unpreima
522. inpreima
523. difpreima
524. respreima
525. cnvimainrn
526. sspreima
527. iinpreima
528. intpreima
529. fimacnvinrn
530. fimacnvinrn2
531. rescnvimafod
532. fvn0ssdmfun
533. fnopfv
534. fvelrn
535. nelrnfvne
536. fveqdmss
537. fveqressseq
538. fnfvelrn
539. ffvelcdm
540. fnfvelrnd
541. ffvelcdmi
542. ffvelcdmda
543. ffvelcdmd
544. feldmfvelcdm
545. rexrn
546. ralrn
547. elrnrexdm
548. elrnrexdmb
549. eldmrexrn
550. eldmrexrnb
551. fvcofneq
552. ralrnmptw
553. rexrnmptw
554. ralrnmpt
555. rexrnmpt
556. f0cli
557. dff2
558. dff3
559. dff4
560. dffo3
561. dffo4
562. dffo5
563. exfo
564. dffo3f
565. foelrn
566. foelrnf
567. foco2
568. fmpt
569. f1ompt
570. fmpti
571. fvmptelcdm
572. fmptd
573. fmpttd
574. fmpt3d
575. fmptdf
576. fompt
577. ffnfv
578. ffnfvf
579. fnfvrnss
580. fcdmssb
581. rnmptss
582. fmpt2d
583. ffvresb
584. fssrescdmd
585. f1oresrab
586. f1ossf1o
587. fmptco
588. fmptcof
589. fmptcos
590. cofmpt
591. fcompt
592. fcoconst
593. fsn
594. fsn2
595. fsng
596. fsn2g
597. xpsng
598. xpprsng
599. xpsn
600. f1o2sn
601. residpr
602. dfmpt
603. fnasrn
604. idref
605. funiun
606. funopsn
607. funop
608. funopdmsn
609. funsndifnop
610. funsneqopb
611. ressnop0
612. fpr
613. fprg
614. ftpg
615. ftp
616. fnressn
617. funressn
618. fressnfv
619. fvrnressn
620. fvressn
621. fvconst
622. fnsnr
623. fnsnbg
624. fnsnb
625. fnsnbOLD
626. fmptsn
627. fmptsng
628. fmptsnd
629. fmptap
630. fmptapd
631. fmptpr
632. fvresi
633. fninfp
634. fnelfp
635. fndifnfp
636. fnelnfp
637. fnnfpeq0
638. fvunsn
639. fvsng
640. fvsn
641. fvsnun1
642. fvsnun2
643. fnsnsplit
644. fsnunf
645. fsnunf2
646. fsnunfv
647. fsnunres
648. funresdfunsn
649. fvpr1g
650. fvpr2g
651. fvpr1
652. fvpr2
653. fprb
654. fvtp1
655. fvtp2
656. fvtp3
657. fvtp1g
658. fvtp2g
659. fvtp3g
660. tpres
661. fvconst2g
662. fconst2g
663. fvconst2
664. fconst2
665. fconst5
666. rnmptc
667. fnprb
668. fntpb
669. fnpr2g
670. fpr2g
671. fconstfv
672. fconst3
673. fconst4
674. resfunexg
675. resiexd
676. fnex
677. fnexd
678. funex
679. opabex
680. mptexg
681. mptexgf
682. mptex
683. mptexd
684. mptrabex
685. fex
686. fexd
687. mptfvmpt
688. eufnfv
689. funfvima
690. funfvima2
691. funfvima2d
692. fnfvima
693. fnfvimad
694. resfvresima
695. funfvima3
696. ralima
697. rexima
698. reximaOLD
699. ralimaOLD
700. fvclss
701. elabrex
702. elabrexg
703. abrexco
704. imaiun
705. imauni
706. fniunfv
707. funiunfv
708. funiunfvf
709. eluniima
710. elunirn
711. elunirnALT
712. fnunirn
713. dff13
714. dff13f
715. f1veqaeq
716. f1cofveqaeq
717. f1cofveqaeqALT
718. dff14i
719. 2f1fvneq
720. f1mpt
721. f1fveq
722. f1elima
723. f1imass
724. f1imaeq
725. f1imapss
726. fpropnf1
727. f1dom3fv3dif
728. f1dom3el3dif
729. dff14a
730. dff14b
731. f1ounsn
732. f12dfv
733. f13dfv
734. dff1o6
735. f1ocnvfv1
736. f1ocnvfv2
737. f1ocnvfv
738. f1ocnvfvb
739. nvof1o
740. nvocnv
741. f1cdmsn
742. fsnex
743. f1prex
744. f1ocnvdm
745. f1ocnvfvrneq
746. fcof1
747. fcofo
748. cbvfo
749. cbvexfo
750. cocan1
751. cocan2
752. fcof1oinvd
753. fcof1od
754. 2fcoidinvd
755. fcof1o
756. 2fvcoidd
757. 2fvidf1od
758. 2fvidinvd
759. foeqcnvco
760. f1eqcocnv
761. fveqf1o
762. f1ocoima
763. nf1const
764. nf1oconst
765. f1ofvswap
766. fvf1pr
767. fliftrel
768. fliftel
769. fliftel1
770. fliftcnv
771. fliftfun
772. fliftfund
773. fliftfuns
774. fliftf
775. fliftval
776. isoeq1
777. isoeq2
778. isoeq3
779. isoeq4
780. isoeq5
781. nfiso
782. isof1o
783. isof1oidb
784. isof1oopb
785. isorel
786. soisores
787. soisoi
788. isoid
789. isocnv
790. isocnv2
791. isocnv3
792. isores2
793. isores1
794. isores3
795. isotr
796. isomin
797. isoini
798. isoini2
799. isofrlem
800. isoselem
801. isofr
802. isose
803. isofr2
804. isopolem
805. isopo
806. isosolem
807. isoso
808. isowe
809. isowe2
810. f1oiso
811. f1oiso2
812. f1owe
813. weniso
814. weisoeq
815. weisoeq2
816. knatar
817. fvresval
818. funeldmb
819. eqfunresadj
820. eqfunressuc
821. fnssintima
822. imaeqsexvOLD
823. imaeqsalvOLD
824. fnimasnd
Cantor's Theorem
1. canth
2. ncanth
Restricted iota (description binder)
1. crio
2. df-riota
3. riotaeqdv
4. riotabidv
5. riotaeqbidv
6. riotaex
7. riotav
8. riotauni
9. nfriota1
10. nfriotadw
11. cbvriotaw
12. cbvriotavw
13. nfriotad
14. nfriota
15. cbvriota
16. cbvriotav
17. csbriota
18. riotacl2
19. riotacl
20. riotasbc
21. riotabidva
22. riotabiia
23. riota1
24. riota1a
25. riota2df
26. riota2f
27. riota2
28. riotaeqimp
29. riotaprop
30. riota5f
31. riota5
32. riotass2
33. riotass
34. moriotass
35. snriota
36. riotaxfrd
37. eusvobj2
38. eusvobj1
39. f1ofveu
40. f1ocnvfv3
41. riotaund
42. riotassuni
43. riotaclb
44. riotarab
Operations
1. co
2. coprab
3. cmpo
4. df-ov
5. df-oprab
6. df-mpo
7. oveq
8. oveq1
9. oveq2
10. oveq12
11. oveq1i
12. oveq2i
13. oveq12i
14. oveqi
15. oveq123i
16. oveq1d
17. oveq2d
18. oveqd
19. oveq12d
20. oveqan12d
21. oveqan12rd
22. oveq123d
23. fvoveq1d
24. fvoveq1
25. ovanraleqv
26. imbrov2fvoveq
27. ovrspc2v
28. oveqrspc2v
29. oveqdr
30. nfovd
31. nfov
32. oprabidw
33. oprabid
34. ovex
35. ovexi
36. ovexd
37. ovssunirn
38. 0ov
39. ovprc
40. ovprc1
41. ovprc2
42. ovrcl
43. elfvov1
44. elfvov2
45. csbov123
46. csbov
47. csbov12g
48. csbov1g
49. csbov2g
50. rspceov
51. elovimad
52. fnbrovb
53. fnotovb
54. opabbrex
55. opabresex2
56. fvmptopab
57. f1opr
58. brfvopab
59. dfoprab2
60. reloprab
61. oprabv
62. nfoprab1
63. nfoprab2
64. nfoprab3
65. nfoprab
66. oprabbid
67. oprabbidv
68. oprabbii
69. ssoprab2
70. ssoprab2b
71. eqoprab2bw
72. eqoprab2b
73. mpoeq123
74. mpoeq12
75. mpoeq123dva
76. mpoeq123dv
77. mpoeq123i
78. mpoeq3dva
79. mpoeq3ia
80. mpoeq3dv
81. nfmpo1
82. nfmpo2
83. nfmpo
84. 0mpo0
85. mpo0v
86. mpo0
87. oprab4
88. cbvoprab1
89. cbvoprab2
90. cbvoprab12
91. cbvoprab12v
92. cbvoprab3
93. cbvoprab3v
94. cbvmpox
95. cbvmpo
96. cbvmpov
97. elimdelov
98. brif1
99. ovif
100. ovif2
101. ovif12
102. ifov
103. ifmpt2v
104. dmoprab
105. dmoprabss
106. rnoprab
107. rnoprab2
108. reldmoprab
109. oprabss
110. eloprabga
111. eloprabg
112. ssoprab2i
113. mpov
114. mpomptx
115. mpompt
116. mpodifsnif
117. mposnif
118. fconstmpo
119. resoprab
120. resoprab2
121. resmpo
122. funoprabg
123. funoprab
124. fnoprabg
125. mpofun
126. fnoprab
127. ffnov
128. fovcld
129. fovcl
130. eqfnov
131. eqfnov2
132. fnov
133. mpo2eqb
134. rnmpo
135. reldmmpo
136. elrnmpog
137. elrnmpo
138. elimampo
139. elrnmpores
140. ralrnmpo
141. rexrnmpo
142. ovid
143. ovidig
144. ovidi
145. ov
146. ovigg
147. ovig
148. ovmpt4g
149. ovmpos
150. ov2gf
151. ovmpodxf
152. ovmpodx
153. ovmpod
154. ovmpox
155. ovmpoga
156. ovmpoa
157. ovmpodf
158. ovmpodv
159. ovmpodv2
160. ovmpog
161. ovmpo
162. ovmpot
163. fvmpopr2d
164. ov3
165. ov6g
166. ovg
167. ovres
168. ovresd
169. oprres
170. oprssov
171. fovcdm
172. fovcdmda
173. fovcdmd
174. fnrnov
175. foov
176. fnovrn
177. ovelrn
178. funimassov
179. ovelimab
180. ovima0
181. ovconst2
182. oprssdm
183. nssdmovg
184. ndmovg
185. ndmov
186. ndmovcl
187. ndmovrcl
188. ndmovcom
189. ndmovass
190. ndmovdistr
191. ndmovord
192. ndmovordi
193. Variable-to-class conversion for operations
Maps-to notation
1. mpondm0
2. elmpocl
3. elmpocl1
4. elmpocl2
5. elovmpod
6. elovmpo
7. elovmporab
8. elovmporab1w
9. elovmporab1
10. 2mpo0
11. relmptopab
12. f1ocnvd
13. f1od
14. f1ocnv2d
15. f1o2d
16. f1opw2
17. f1opw
18. elovmpt3imp
19. ovmpt3rab1
20. ovmpt3rabdm
21. elovmpt3rab1
22. elovmpt3rab
Function operation
1. cof
2. cofr
3. df-of
4. df-ofr
5. ofeqd
6. ofeq
7. ofreq
8. ofexg
9. nfof
10. nfofr
11. ofrfvalg
12. offval
13. ofrfval
14. ofval
15. ofrval
16. offn
17. offun
18. offval2f
19. ofmresval
20. fnfvof
21. off
22. ofres
23. offval2
24. ofrfval2
25. offvalfv
26. ofmpteq
27. coof
28. ofco
29. offveq
30. offveqb
31. ofc1
32. ofc2
33. ofc12
34. caofref
35. caofinvl
36. caofid0l
37. caofid0r
38. caofid1
39. caofid2
40. caofcom
41. caofidlcan
42. caofrss
43. caofass
44. caoftrn
45. caofdi
46. caofdir
47. caonncan
Proper subset relation
1. crpss
2. df-rpss
3. relrpss
4. brrpssg
5. brrpss
6. porpss
7. sorpss
8. sorpssi
9. sorpssun
10. sorpssin
11. sorpssuni
12. sorpssint
13. sorpsscmpl