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. moabexOLD
41. rmorabex
42. euabex
43. nnullss
44. exss
45. opex
46. otex
47. elopg
48. elop
49. opi1
50. opi2
51. opeluu
52. op1stb
53. 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. xp0
104. csbxp
105. releq
106. releqi
107. releqd
108. nfrel
109. sbcrel
110. relss
111. ssrel
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. inxp
160. inxpOLD
161. xpindi
162. xpindir
163. xpiindi
164. xpriindi
165. eliunxp
166. opeliunxp2
167. raliunxp
168. rexiunxp
169. ralxp
170. rexxp
171. exopxfr
172. exopxfr2
173. djussxp
174. ralxpf
175. rexxpf
176. iunxpf
177. opabbi2dv
178. relop
179. ideqg
180. ideq
181. ididg
182. issetid
183. coss1
184. coss2
185. coeq1
186. coeq2
187. coeq1i
188. coeq2i
189. coeq1d
190. coeq2d
191. coeq12i
192. coeq12d
193. nfco
194. brcog
195. opelco2g
196. brcogw
197. eqbrrdva
198. brco
199. opelco
200. cnvss
201. cnveq
202. cnveqi
203. cnveqd
204. elcnv
205. elcnv2
206. nfcnv
207. brcnvg
208. opelcnvg
209. opelcnv
210. brcnv
211. csbcnv
212. csbcnvgALT
213. cnvco
214. cnvuni
215. dfdm3
216. dfrn2
217. dfrn3
218. elrn2g
219. elrng
220. elrn2
221. elrn
222. ssrelrn
223. dfdm4
224. dfdmf
225. csbdm
226. eldmg
227. eldm2g
228. eldm
229. eldm2
230. dmss
231. dmeq
232. dmeqi
233. dmeqd
234. opeldmd
235. opeldm
236. breldm
237. breldmg
238. dmun
239. dmin
240. breldmd
241. dmiun
242. dmuni
243. dmopab
244. dmopabelb
245. dmopab2rex
246. dmopabss
247. dmopab3
248. dm0
249. dmi
250. dmv
251. dmep
252. dm0rn0
253. dm0rn0OLD
254. rn0
255. rnep
256. reldm0
257. dmxp
258. dmxpid
259. dmxpin
260. xpid11
261. dmcnvcnv
262. rncnvcnv
263. elreldm
264. rneq
265. rneqi
266. rneqd
267. rnss
268. rnssi
269. brelrng
270. brelrn
271. opelrn
272. releldm
273. relelrn
274. releldmb
275. relelrnb
276. releldmi
277. relelrni
278. dfrnf
279. nfdm
280. nfrn
281. dmiin
282. rnopab
283. rnopabss
284. rnopab3
285. rnmpt
286. elrnmpt
287. elrnmpt1s
288. elrnmpt1
289. elrnmptg
290. elrnmpti
291. elrnmptd
292. elrnmpt1d
293. elrnmptdv
294. elrnmpt2d
295. nelrnmpt
296. dfiun3g
297. dfiin3g
298. dfiun3
299. dfiin3
300. riinint
301. relrn0
302. dmrnssfld
303. dmcoss
304. dmcossOLD
305. rncoss
306. dmcosseq
307. dmcosseqOLD
308. dmcosseqOLDOLD
309. dmcoeq
310. rncoeq
311. reseq1
312. reseq2
313. reseq1i
314. reseq2i
315. reseq12i
316. reseq1d
317. reseq2d
318. reseq12d
319. nfres
320. csbres
321. res0
322. dfres3
323. opelres
324. brres
325. opelresi
326. brresi
327. opres
328. resieq
329. opelidres
330. resres
331. resundi
332. resundir
333. resindi
334. resindir
335. inres
336. resdifcom
337. resiun1
338. resiun2
339. resss
340. rescom
341. ssres
342. ssres2
343. relres
344. resabs1
345. resabs1i
346. resabs1d
347. resabs2
348. residm
349. dmresss
350. dmres
351. ssdmres
352. dmresexg
353. resima
354. resima2
355. rnresss
356. xpssres
357. elinxp
358. elres
359. elsnres
360. relssres
361. dmressnsn
362. eldmressnsn
363. eldmeldmressn
364. resdm
365. resexg
366. resexd
367. resex
368. resindm
369. resdmdfsn
370. reldisjun
371. relresdm1
372. resopab
373. iss
374. resopab2
375. resmpt
376. resmpt3
377. resmptf
378. resmptd
379. dfres2
380. mptss
381. elimampt
382. elidinxp
383. elidinxpid
384. elrid
385. idinxpres
386. idinxpresid
387. idssxp
388. opabresid
389. mptresid
390. dmresi
391. restidsing
392. iresn0n0
393. imaeq1
394. imaeq2
395. imaeq1i
396. imaeq2i
397. imaeq1d
398. imaeq2d
399. imaeq12d
400. dfima2
401. dfima3
402. elimag
403. elima
404. elima2
405. elima3
406. nfima
407. nfimad
408. imadmrn
409. imassrn
410. mptima
411. mptimass
412. imai
413. rnresi
414. resiima
415. ima0
416. 0ima
417. csbima12
418. imadisj
419. imadisjlnd
420. cnvimass
421. cnvimarndm
422. imasng
423. relimasn
424. elrelimasn
425. elimasng1
426. elimasn1
427. elimasng
428. elimasn
429. elimasni
430. args
431. elinisegg
432. eliniseg
433. epin
434. epini
435. iniseg
436. inisegn0
437. dffr3
438. dfse2
439. imass1
440. imass2
441. ndmima
442. relcnv
443. relbrcnvg
444. eliniseg2
445. relbrcnv
446. relco
447. cotrg
448. cotr
449. idrefALT
450. cnvsym
451. intasym
452. asymref
453. asymref2
454. intirr
455. brcodir
456. codir
457. qfto
458. xpidtr
459. trin2
460. poirr2
461. trinxp
462. soirri
463. sotri
464. son2lpi
465. sotri2
466. sotri3
467. poleloe
468. poltletr
469. somin1
470. somincom
471. somin2
472. soltmin
473. cnvopab
474. cnvopabOLD
475. mptcnv
476. cnv0
477. cnv0OLD
478. cnvi
479. cnvun
480. cnvdif
481. cnvin
482. rnun
483. rnin
484. rniun
485. rnuni
486. imaundi
487. imaundir
488. imadifssran
489. cnvimassrndm
490. dminss
491. imainss
492. inimass
493. inimasn
494. cnvxp
495. xp0OLD
496. xpnz
497. xpeq0
498. xpdisj1
499. xpdisj2
500. xpsndisj
501. difxp
502. difxp1
503. difxp2
504. djudisj
505. xpdifid
506. resdisj
507. rnxp
508. dmxpss
509. rnxpss
510. rnxpid
511. ssxpb
512. xp11
513. xpcan
514. xpcan2
515. ssrnres
516. rninxp
517. dminxp
518. imainrect
519. xpima
520. xpima1
521. xpima2
522. xpimasn
523. sossfld
524. sofld
525. cnvcnv3
526. dfrel2
527. dfrel4v
528. dfrel4
529. cnvcnv
530. cnvcnv2
531. cnvcnvss
532. cnvrescnv
533. cnveqb
534. cnveq0
535. dfrel3
536. elid
537. dmresv
538. rnresv
539. dfrn4
540. csbrn
541. rescnvcnv
542. cnvcnvres
543. imacnvcnv
544. dmsnn0
545. rnsnn0
546. dmsn0
547. cnvsn0
548. dmsn0el
549. relsn2
550. dmsnopg
551. dmsnopss
552. dmpropg
553. dmsnop
554. dmprop
555. dmtpop
556. cnvcnvsn
557. dmsnsnsn
558. rnsnopg
559. rnpropg
560. cnvsng
561. rnsnop
562. op1sta
563. cnvsn
564. op2ndb
565. op2nda
566. opswap
567. cnvresima
568. resdm2
569. resdmres
570. resresdm
571. imadmres
572. resdmss
573. resdifdi
574. resdifdir
575. mptpreima
576. mptiniseg
577. dmmpt
578. dmmptss
579. dmmptg
580. rnmpt0f
581. rnmptn0
582. dfco2
583. dfco2a
584. coundi
585. coundir
586. cores
587. resco
588. imaco
589. rnco
590. rncoOLD
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. resssxp
608. cnvssrndm
609. cossxp
610. relrelss
611. unielrel
612. relfld
613. relresfld
614. relcoi2
615. relcoi1
616. unidmrn
617. relcnvfld
618. dfdm2
619. unixp
620. unixp0
621. unixpid
622. ressn
623. cnviin
624. cnvpo
625. cnvso
626. xpco
627. xpcoid
628. elsnxp
629. reu3op
630. reuop
631. opreu2reurex
632. opreu2reu
633. dfpo2
634. csbcog
635. snres0
636. 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. f1oiOLD
329. f1ovi
330. f1osn
331. f1osng
332. f1sng
333. fsnd
334. f1oprswap
335. f1oprg
336. tz6.12-2
337. tz6.12-2OLD
338. fveu
339. brprcneu
340. brprcneuALT
341. fvprc
342. fvprcALT
343. rnfvprc
344. fv2
345. dffv3
346. dffv4
347. elfv
348. fveq1
349. fveq2
350. fveq1i
351. fveq1d
352. fveq2i
353. fveq2d
354. 2fveq3
355. fveq12i
356. fveq12d
357. fveqeq2d
358. fveqeq2
359. nffv
360. nffvmpt1
361. nffvd
362. fvex
363. fvexi
364. fvexd
365. fvif
366. iffv
367. fv3
368. fvres
369. fvresd
370. funssfv
371. tz6.12c
372. tz6.12-1
373. tz6.12
374. tz6.12f
375. tz6.12i
376. fvbr0
377. fvrn0
378. fvn0fvelrn
379. elfvunirn
380. fvssunirn
381. ndmfv
382. ndmfvrcl
383. elfvdm
384. elfvex
385. elfvexd
386. eliman0
387. nfvres
388. nfunsn
389. fvfundmfvn0
390. 0fv
391. fv2prc
392. elfv2ex
393. fveqres
394. csbfv12
395. csbfv2g
396. csbfv
397. funbrfv
398. funopfv
399. fnbrfvb
400. fnopfvb
401. fvelima2
402. funbrfvb
403. funopfvb
404. fnbrfvb2
405. fdmeu
406. funbrfv2b
407. dffn5
408. fnrnfv
409. fvelrnb
410. foelcdmi
411. dfimafn
412. dfimafn2
413. funimass4
414. fvelima
415. funimassd
416. fvelimad
417. feqmptd
418. feqresmpt
419. feqmptdf
420. dffn5f
421. fvelimab
422. fvelimabd
423. fimarab
424. unima
425. fvi
426. fviss
427. fniinfv
428. fnsnfv
429. opabiotafun
430. opabiotadm
431. opabiota
432. fnimapr
433. fnimatpd
434. ssimaex
435. ssimaexg
436. funfv
437. funfv2
438. funfv2f
439. fvun
440. fvun1
441. fvun2
442. fvun1d
443. fvun2d
444. dffv2
445. dmfco
446. fvco2
447. fvco
448. fvco3
449. fvco3d
450. fvco4i
451. fvopab3g
452. fvopab3ig
453. brfvopabrbr
454. fvmptg
455. fvmpti
456. fvmpt
457. fvmpt2f
458. fvtresfn
459. fvmpts
460. fvmpt3
461. fvmpt3i
462. fvmptdf
463. fvmptd
464. fvmptd2
465. mptrcl
466. fvmpt2i
467. fvmpt2
468. fvmptss
469. fvmpt2d
470. fvmptex
471. fvmptd3f
472. fvmptd2f
473. fvmptdv
474. fvmptdv2
475. mpteqb
476. fvmptt
477. fvmptf
478. fvmptnf
479. fvmptd3
480. fvmptd4
481. fvmptn
482. fvmptss2
483. elfvmptrab1w
484. elfvmptrab1
485. elfvmptrab
486. fvopab4ndm
487. fvmptndm
488. fvmptrabfv
489. fvopab5
490. fvopab6
491. eqfnfv
492. eqfnfv2
493. eqfnfv3
494. eqfnfvd
495. eqfnfv2f
496. eqfunfv
497. eqfnun
498. fvreseq0
499. fvreseq1
500. fvreseq
501. fnmptfvd
502. fndmdif
503. fndmdifcom
504. fndmdifeq0
505. fndmin
506. fneqeql
507. fneqeql2
508. fnreseql
509. chfnrn
510. funfvop
511. funfvbrb
512. fvimacnvi
513. fvimacnv
514. funimass3
515. funimass5
516. funconstss
517. fvimacnvALT
518. elpreima
519. elpreimad
520. fniniseg
521. fncnvima2
522. fniniseg2
523. unpreima
524. inpreima
525. difpreima
526. respreima
527. cnvimainrn
528. sspreima
529. iinpreima
530. intpreima
531. fimacnvinrn
532. fimacnvinrn2
533. rescnvimafod
534. fvn0ssdmfun
535. fnopfv
536. fvelrn
537. nelrnfvne
538. fveqdmss
539. fveqressseq
540. fnfvelrn
541. ffvelcdm
542. fnfvelrnd
543. ffvelcdmi
544. ffvelcdmda
545. ffvelcdmd
546. feldmfvelcdm
547. rexrn
548. ralrn
549. elrnrexdm
550. elrnrexdmb
551. eldmrexrn
552. eldmrexrnb
553. fvcofneq
554. ralrnmptw
555. rexrnmptw
556. ralrnmpt
557. rexrnmpt
558. f0cli
559. dff2
560. dff3
561. dff4
562. dffo3
563. dffo4
564. dffo5
565. exfo
566. dffo3f
567. foelrn
568. foelrnf
569. foco2
570. fmpt
571. f1ompt
572. fmpti
573. fvmptelcdm
574. fmptd
575. fmpttd
576. fmpt3d
577. fmptdf
578. fompt
579. ffnfv
580. ffnfvf
581. fnfvrnss
582. fcdmssb
583. rnmptss
584. fmpt2d
585. ffvresb
586. fssrescdmd
587. f1oresrab
588. f1ossf1o
589. fmptco
590. fmptcof
591. fmptcos
592. cofmpt
593. fcompt
594. fcoconst
595. fsn
596. fsn2
597. fsng
598. fsn2g
599. xpsng
600. xpprsng
601. xpsn
602. f1o2sn
603. residpr
604. dfmpt
605. fnasrn
606. idref
607. funiun
608. funopsn
609. funop
610. funopdmsn
611. funsndifnop
612. funsneqopb
613. ressnop0
614. fpr
615. fprg
616. ftpg
617. ftp
618. fnressn
619. funressn
620. fressnfv
621. fvrnressn
622. fvressn
623. fvconst
624. fnsnr
625. fnsnbg
626. fnsnb
627. fnsnbOLD
628. fmptsn
629. fmptsng
630. fmptsnd
631. fmptap
632. fmptapd
633. fmptpr
634. fvresi
635. fninfp
636. fnelfp
637. fndifnfp
638. fnelnfp
639. fnnfpeq0
640. fvunsn
641. fvsng
642. fvsn
643. fvsnun1
644. fvsnun2
645. fnsnsplit
646. fsnunf
647. fsnunf2
648. fsnunfv
649. fsnunres
650. funresdfunsn
651. fvpr1g
652. fvpr2g
653. fvpr1
654. fvpr2
655. fprb
656. fvtp1
657. fvtp2
658. fvtp3
659. fvtp1g
660. fvtp2g
661. fvtp3g
662. tpres
663. fvconst2g
664. fconst2g
665. fvconst2
666. fconst2
667. fconst5
668. rnmptc
669. fnprb
670. fntpb
671. fnpr2g
672. fpr2g
673. fconstfv
674. fconst3
675. fconst4
676. resfunexg
677. resiexd
678. fnex
679. fnexd
680. funex
681. opabex
682. mptexg
683. mptexgf
684. mptex
685. mptexd
686. mptrabex
687. fex
688. fexd
689. mptfvmpt
690. eufnfv
691. funfvima
692. funfvima2
693. funfvima2d
694. fnfvima
695. fnfvimad
696. resfvresima
697. funfvima3
698. ralima
699. rexima
700. reximaOLD
701. ralimaOLD
702. fvclss
703. elabrex
704. elabrexg
705. abrexco
706. imaiun
707. imauni
708. fniunfv
709. funiunfv
710. funiunfvf
711. eluniima
712. elunirn
713. elunirnALT
714. fnunirn
715. dff13
716. dff13f
717. f1veqaeq
718. f1cofveqaeq
719. f1cofveqaeqALT
720. dff14i
721. 2f1fvneq
722. f1mpt
723. f1fveq
724. f1elima
725. f1imass
726. f1imaeq
727. f1imapss
728. fpropnf1
729. f1dom3fv3dif
730. f1dom3el3dif
731. dff14a
732. dff14b
733. f1ounsn
734. f12dfv
735. f13dfv
736. dff1o6
737. f1ocnvfv1
738. f1ocnvfv2
739. f1ocnvfv
740. f1ocnvfvb
741. nvof1o
742. nvocnv
743. f1cdmsn
744. fsnex
745. f1prex
746. f1ocnvdm
747. f1ocnvfvrneq
748. fcof1
749. fcofo
750. cbvfo
751. cbvexfo
752. cocan1
753. cocan2
754. fcof1oinvd
755. fcof1od
756. 2fcoidinvd
757. fcof1o
758. 2fvcoidd
759. 2fvidf1od
760. 2fvidinvd
761. foeqcnvco
762. f1eqcocnv
763. fveqf1o
764. f1ocoima
765. nf1const
766. nf1oconst
767. f1ofvswap
768. fvf1pr
769. fliftrel
770. fliftel
771. fliftel1
772. fliftcnv
773. fliftfun
774. fliftfund
775. fliftfuns
776. fliftf
777. fliftval
778. isoeq1
779. isoeq2
780. isoeq3
781. isoeq4
782. isoeq5
783. nfiso
784. isof1o
785. isof1oidb
786. isof1oopb
787. isorel
788. soisores
789. soisoi
790. isoid
791. isocnv
792. isocnv2
793. isocnv3
794. isores2
795. isores1
796. isores3
797. isotr
798. isomin
799. isoini
800. isoini2
801. isofrlem
802. isoselem
803. isofr
804. isose
805. isofr2
806. isopolem
807. isopo
808. isosolem
809. isoso
810. isowe
811. isowe2
812. f1oiso
813. f1oiso2
814. f1owe
815. weniso
816. weisoeq
817. weisoeq2
818. knatar
819. fvresval
820. funeldmb
821. eqfunresadj
822. eqfunressuc
823. fnssintima
824. imaeqsexvOLD
825. imaeqsalvOLD
826. 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