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. copsex4g
22. 0nelop
23. opwo0id
24. opeqex
25. oteqex2
26. oteqex
27. opcom
28. moop2
29. opeqsng
30. opeqsn
31. opeqpr
32. snopeqop
33. propeqop
34. propssopi
35. snopeqopsnid
36. mosubopt
37. mosubop
38. euop2
39. euotd
40. opthwiener
41. uniop
42. uniopel
43. opthhausdorff
44. opthhausdorff0
45. otsndisj
46. otiunsndisj
47. iunopeqop
Ordered-pair class abstractions (cont.)
1. opabidw
2. opabid
3. elopab
4. rexopabb
5. opelopabsbALT
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. rabxp
49. brxp
50. pwvrel
51. pwvabrel
52. brrelex12
53. brrelex1
54. brrelex2
55. brrelex12i
56. brrelex1i
57. brrelex2i
58. nprrel12
59. nprrel
60. 0nelrel0
61. 0nelrel
62. fconstmpt
63. vtoclr
64. opthprc
65. brel
66. elxp3
67. opeliunxp
68. xpundi
69. xpundir
70. xpiundi
71. xpiundir
72. iunxpconst
73. xpun
74. elvv
75. elvvv
76. elvvuni
77. brinxp2
78. brinxp
79. opelinxp
80. poinxp
81. soinxp
82. frinxp
83. seinxp
84. weinxp
85. posn
86. sosn
87. frsn
88. wesn
89. elopaelxp
90. bropaex12
91. opabssxp
92. brab2a
93. optocl
94. 2optocl
95. 3optocl
96. opbrop
97. 0xp
98. csbxp
99. releq
100. releqi
101. releqd
102. nfrel
103. sbcrel
104. relss
105. ssrel
106. eqrel
107. ssrel2
108. relssi
109. relssdv
110. eqrelriv
111. eqrelriiv
112. eqbrriv
113. eqrelrdv
114. eqbrrdv
115. eqbrrdiv
116. eqrelrdv2
117. ssrelrel
118. eqrelrel
119. elrel
120. rel0
121. nrelv
122. relsng
123. relsnb
124. relsnopg
125. relsn
126. relsnop
127. copsex2gb
128. copsex2ga
129. elopaba
130. xpsspw
131. unixpss
132. relun
133. relin1
134. relin2
135. relinxp
136. reldif
137. reliun
138. reliin
139. reluni
140. relint
141. relopabiv
142. relopabi
143. relopabiALT
144. relopab
145. mptrel
146. reli
147. rele
148. opabid2
149. inopab
150. difopab
151. inxp
152. xpindi
153. xpindir
154. xpiindi
155. xpriindi
156. eliunxp
157. opeliunxp2
158. raliunxp
159. rexiunxp
160. ralxp
161. rexxp
162. exopxfr
163. exopxfr2
164. djussxp
165. ralxpf
166. rexxpf
167. iunxpf
168. opabbi2dv
169. relop
170. ideqg
171. ideq
172. ididg
173. issetid
174. coss1
175. coss2
176. coeq1
177. coeq2
178. coeq1i
179. coeq2i
180. coeq1d
181. coeq2d
182. coeq12i
183. coeq12d
184. nfco
185. brcog
186. opelco2g
187. brcogw
188. eqbrrdva
189. brco
190. opelco
191. cnvss
192. cnveq
193. cnveqi
194. cnveqd
195. elcnv
196. elcnv2
197. nfcnv
198. brcnvg
199. opelcnvg
200. opelcnv
201. brcnv
202. csbcnv
203. csbcnvgALT
204. cnvco
205. cnvuni
206. dfdm3
207. dfrn2
208. dfrn3
209. elrn2g
210. elrng
211. ssrelrn
212. dfdm4
213. dfdmf
214. csbdm
215. eldmg
216. eldm2g
217. eldm
218. eldm2
219. dmss
220. dmeq
221. dmeqi
222. dmeqd
223. opeldmd
224. opeldm
225. breldm
226. breldmg
227. dmun
228. dmin
229. breldmd
230. dmiun
231. dmuni
232. dmopab
233. dmopabelb
234. dmopab2rex
235. dmopabss
236. dmopab3
237. opabssxpd
238. dm0
239. dmi
240. dmv
241. dmep
242. domepOLD
243. dm0rn0
244. rn0
245. rnep
246. reldm0
247. dmxp
248. dmxpid
249. dmxpin
250. xpid11
251. dmcnvcnv
252. rncnvcnv
253. elreldm
254. rneq
255. rneqi
256. rneqd
257. rnss
258. rnssi
259. brelrng
260. brelrn
261. opelrn
262. releldm
263. relelrn
264. releldmb
265. relelrnb
266. releldmi
267. relelrni
268. dfrnf
269. elrn2
270. elrn
271. nfdm
272. nfrn
273. dmiin
274. rnopab
275. rnmpt
276. elrnmpt
277. elrnmpt1s
278. elrnmpt1
279. elrnmptg
280. elrnmpti
281. elrnmptd
282. elrnmptdv
283. elrnmpt2d
284. dfiun3g
285. dfiin3g
286. dfiun3
287. dfiin3
288. riinint
289. relrn0
290. dmrnssfld
291. dmcoss
292. rncoss
293. dmcosseq
294. dmcoeq
295. rncoeq
296. reseq1
297. reseq2
298. reseq1i
299. reseq2i
300. reseq12i
301. reseq1d
302. reseq2d
303. reseq12d
304. nfres
305. csbres
306. res0
307. dfres3
308. opelres
309. brres
310. opelresi
311. brresi
312. opres
313. resieq
314. opelidres
315. resres
316. resundi
317. resundir
318. resindi
319. resindir
320. inres
321. resdifcom
322. resiun1
323. resiun2
324. dmres
325. ssdmres
326. dmresexg
327. resss
328. rescom
329. ssres
330. ssres2
331. relres
332. resabs1
333. resabs1d
334. resabs2
335. residm
336. resima
337. resima2
338. rnresss
339. xpssres
340. elinxp
341. elres
342. elsnres
343. relssres
344. dmressnsn
345. eldmressnsn
346. eldmeldmressn
347. resdm
348. resexg
349. resexd
350. resex
351. resindm
352. resdmdfsn
353. resopab
354. iss
355. resopab2
356. resmpt
357. resmpt3
358. resmptf
359. resmptd
360. dfres2
361. mptss
362. elidinxp
363. elidinxpid
364. elrid
365. idinxpres
366. idinxpresid
367. idssxp
368. opabresid
369. mptresid
370. opabresidOLD
371. mptresidOLD
372. dmresi
373. restidsing
374. iresn0n0
375. imaeq1
376. imaeq2
377. imaeq1i
378. imaeq2i
379. imaeq1d
380. imaeq2d
381. imaeq12d
382. dfima2
383. dfima3
384. elimag
385. elima
386. elima2
387. elima3
388. nfima
389. nfimad
390. imadmrn
391. imassrn
392. mptima
393. imai
394. rnresi
395. resiima
396. ima0
397. 0ima
398. csbima12
399. imadisj
400. cnvimass
401. cnvimarndm
402. imasng
403. relimasn
404. elrelimasn
405. elimasn
406. elimasng
407. elimasni
408. args
409. eliniseg
410. epini
411. iniseg
412. inisegn0
413. dffr3
414. dfse2
415. imass1
416. imass2
417. ndmima
418. relcnv
419. relbrcnvg
420. eliniseg2
421. relbrcnv
422. cotrg
423. cotr
424. idrefALT
425. cnvsym
426. intasym
427. asymref
428. asymref2
429. intirr
430. brcodir
431. codir
432. qfto
433. xpidtr
434. trin2
435. poirr2
436. trinxp
437. soirri
438. sotri
439. son2lpi
440. sotri2
441. sotri3
442. poleloe
443. poltletr
444. somin1
445. somincom
446. somin2
447. soltmin
448. cnvopab
449. mptcnv
450. cnv0
451. cnvi
452. cnvun
453. cnvdif
454. cnvin
455. rnun
456. rnin
457. rniun
458. rnuni
459. imaundi
460. imaundir
461. dminss
462. imainss
463. inimass
464. inimasn
465. cnvxp
466. xp0
467. xpnz
468. xpeq0
469. xpdisj1
470. xpdisj2
471. xpsndisj
472. difxp
473. difxp1
474. difxp2
475. djudisj
476. xpdifid
477. resdisj
478. rnxp
479. dmxpss
480. rnxpss
481. rnxpid
482. ssxpb
483. xp11
484. xpcan
485. xpcan2
486. ssrnres
487. rninxp
488. dminxp
489. imainrect
490. xpima
491. xpima1
492. xpima2
493. xpimasn
494. sossfld
495. sofld
496. cnvcnv3
497. dfrel2
498. dfrel4v
499. dfrel4
500. cnvcnv
501. cnvcnv2
502. cnvcnvss
503. cnvrescnv
504. cnveqb
505. cnveq0
506. dfrel3
507. elid
508. dmresv
509. rnresv
510. dfrn4
511. csbrn
512. rescnvcnv
513. cnvcnvres
514. imacnvcnv
515. dmsnn0
516. rnsnn0
517. dmsn0
518. cnvsn0
519. dmsn0el
520. relsn2
521. dmsnopg
522. dmsnopss
523. dmpropg
524. dmsnop
525. dmprop
526. dmtpop
527. cnvcnvsn
528. dmsnsnsn
529. rnsnopg
530. rnpropg
531. cnvsng
532. rnsnop
533. op1sta
534. cnvsn
535. op2ndb
536. op2nda
537. opswap
538. cnvresima
539. resdm2
540. resdmres
541. resresdm
542. imadmres
543. mptpreima
544. mptiniseg
545. dmmpt
546. dmmptss
547. dmmptg
548. relco
549. dfco2
550. dfco2a
551. coundi
552. coundir
553. cores
554. resco
555. imaco
556. rnco
557. rnco2
558. dmco
559. coeq0
560. coiun
561. cocnvcnv1
562. cocnvcnv2
563. cores2
564. co02
565. co01
566. coi1
567. coi2
568. coires1
569. coass
570. relcnvtrg
571. relcnvtr
572. relssdmrn
573. resssxp
574. cnvssrndm
575. cossxp
576. relrelss
577. unielrel
578. relfld
579. relresfld
580. relcoi2
581. relcoi1
582. unidmrn
583. relcnvfld
584. dfdm2
585. unixp
586. unixp0
587. unixpid
588. ressn
589. cnviin
590. cnvpo
591. cnvso
592. xpco
593. xpcoid
594. elsnxp
595. reu3op
596. reuop
597. opreu2reurex
598. 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. onordi
107. ontrci
108. onirri
109. oneli
110. onelssi
111. onssneli
112. onssnel2i
113. onelini
114. oneluni
115. onunisuci
116. onsseli
117. onun2i
118. unizlim
119. on0eqel
120. snsn0non
121. onxpdisj
122. onnev
123. 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. cbviota
13. cbviotav
14. sb8iota
15. iotaeq
16. iotabi
17. uniabio
18. iotaval
19. iotauni
20. iotaint
21. iota1
22. iotanul
23. iotassuni
24. iotaex
25. iota4
26. iota4an
27. iota5
28. iotabidv
29. iotabii
30. iotacl
31. iota2df
32. iota2d
33. iota2
34. iotan0
35. sniota
36. dfiota4
37. 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. fnunsn
120. fnco
121. fnresdm
122. fnresdisj
123. 2elresin
124. fnssresb
125. fnssres
126. fnssresd
127. fnresin1
128. fnresin2
129. fnres
130. idfn
131. fnresi
132. fnresiOLD
133. fnima
134. fn0
135. fnimadisj
136. fnimaeq0
137. dfmpt3
138. mptfnf
139. fnmptf
140. fnopabg
141. fnopab
142. mptfng
143. fnmpt
144. fnmptd
145. mpt0
146. fnmpti
147. dmmpti
148. dmmptd
149. mptun
150. partfun
151. feq1
152. feq2
153. feq3
154. feq23
155. feq1d
156. feq2d
157. feq3d
158. feq12d
159. feq123d
160. feq123
161. feq1i
162. feq2i
163. feq12i
164. feq23i
165. feq23d
166. nff
167. sbcfng
168. sbcfg
169. elimf
170. ffn
171. ffnd
172. dffn2
173. ffun
174. ffund
175. frel
176. frn
177. frnd
178. fdm
179. fdmOLD
180. fdmd
181. fdmi
182. dffn3
183. ffrn
184. fss
185. fssd
186. fssdmd
187. fssdm
188. fco
189. fcod
190. fco2
191. fssxp
192. funssxp
193. ffdm
194. ffdmd
195. fdmrn
196. opelf
197. fun
198. fun2
199. fun2d
200. fnfco
201. fssres
202. fssresd
203. fssres2
204. fresin
205. resasplit
206. fresaun
207. fresaunres2
208. fresaunres1
209. fcoi1
210. fcoi2
211. feu
212. fimass
213. fcnvres
214. fimacnvdisj
215. fint
216. fin
217. f0
218. f00
219. f0bi
220. f0dom0
221. f0rn0
222. fconst
223. fconstg
224. fnconstg
225. fconst6g
226. fconst6
227. f1eq1
228. f1eq2
229. f1eq3
230. nff1
231. dff12
232. f1f
233. f1fn
234. f1fun
235. f1rel
236. f1dm
237. f1dmOLD
238. f1ss
239. f1ssr
240. f1ssres
241. f1resf1
242. f1cnvcnv
243. f1co
244. foeq1
245. foeq2
246. foeq3
247. nffo
248. fof
249. fofun
250. fofn
251. forn
252. dffo2
253. foima
254. dffn4
255. funforn
256. fodmrnu
257. fimadmfo
258. fores
259. fimadmfoALT
260. foco
261. foconst
262. f1oeq1
263. f1oeq2
264. f1oeq3
265. f1oeq23
266. f1eq123d
267. foeq123d
268. f1oeq123d
269. f1oeq2d
270. f1oeq3d
271. nff1o
272. f1of1
273. f1of
274. f1ofn
275. f1ofun
276. f1orel
277. f1odm
278. dff1o2
279. dff1o3
280. f1ofo
281. dff1o4
282. dff1o5
283. f1orn
284. f1f1orn
285. f1ocnv
286. f1ocnvb
287. f1ores
288. f1orescnv
289. f1imacnv
290. foimacnv
291. foun
292. f1oun
293. resdif
294. resin
295. f1oco
296. f1cnv
297. funcocnv2
298. fococnv2
299. f1ococnv2
300. f1cocnv2
301. f1ococnv1
302. f1cocnv1
303. funcoeqres
304. f1ssf1
305. f10
306. f10d
307. f1o00
308. fo00
309. f1o0
310. f1oi
311. f1ovi
312. f1osn
313. f1osng
314. f1sng
315. fsnd
316. f1oprswap
317. f1oprg
318. tz6.12-2
319. fveu
320. brprcneu
321. fvprc
322. rnfvprc
323. fv2
324. dffv3
325. dffv4
326. elfv
327. fveq1
328. fveq2
329. fveq1i
330. fveq1d
331. fveq2i
332. fveq2d
333. 2fveq3
334. fveq12i
335. fveq12d
336. fveqeq2d
337. fveqeq2
338. nffv
339. nffvmpt1
340. nffvd
341. fvex
342. fvexi
343. fvexd
344. fvif
345. iffv
346. fv3
347. fvres
348. fvresd
349. funssfv
350. tz6.12-1
351. tz6.12
352. tz6.12f
353. tz6.12c
354. tz6.12i
355. fvbr0
356. fvrn0
357. fvssunirn
358. ndmfv
359. ndmfvrcl
360. elfvdm
361. elfvex
362. elfvexd
363. eliman0
364. nfvres
365. nfunsn
366. fvfundmfvn0
367. 0fv
368. fv2prc
369. elfv2ex
370. fveqres
371. csbfv12
372. csbfv2g
373. csbfv
374. funbrfv
375. funopfv
376. fnbrfvb
377. fnopfvb
378. funbrfvb
379. funopfvb
380. fnbrfvb2
381. funbrfv2b
382. dffn5
383. fnrnfv
384. fvelrnb
385. foelrni
386. dfimafn
387. dfimafn2
388. funimass4
389. fvelima
390. fvelimad
391. feqmptd
392. feqresmpt
393. feqmptdf
394. dffn5f
395. fvelimab
396. fvelimabd
397. unima
398. fvi
399. fviss
400. fniinfv
401. fnsnfv
402. opabiotafun
403. opabiotadm
404. opabiota
405. fnimapr
406. ssimaex
407. ssimaexg
408. funfv
409. funfv2
410. funfv2f
411. fvun
412. fvun1
413. fvun2
414. fvun1d
415. fvun2d
416. dffv2
417. dmfco
418. fvco2
419. fvco
420. fvco3
421. fvco3d
422. fvco4i
423. fvopab3g
424. fvopab3ig
425. brfvopabrbr
426. fvmptg
427. fvmpti
428. fvmpt
429. fvmpt2f
430. fvtresfn
431. fvmpts
432. fvmpt3
433. fvmpt3i
434. fvmptdf
435. fvmptd
436. fvmptd2
437. mptrcl
438. fvmpt2i
439. fvmpt2
440. fvmptss
441. fvmpt2d
442. fvmptex
443. fvmptd3f
444. fvmptd2f
445. fvmptdv
446. fvmptdv2
447. mpteqb
448. fvmptt
449. fvmptf
450. fvmptnf
451. fvmptd3
452. fvmptn
453. fvmptss2
454. elfvmptrab1w
455. elfvmptrab1
456. elfvmptrab
457. fvopab4ndm
458. fvmptndm
459. fvmptrabfv
460. fvopab5
461. fvopab6
462. eqfnfv
463. eqfnfv2
464. eqfnfv3
465. eqfnfvd
466. eqfnfv2f
467. eqfunfv
468. fvreseq0
469. fvreseq1
470. fvreseq
471. fnmptfvd
472. fndmdif
473. fndmdifcom
474. fndmdifeq0
475. fndmin
476. fneqeql
477. fneqeql2
478. fnreseql
479. chfnrn
480. funfvop
481. funfvbrb
482. fvimacnvi
483. fvimacnv
484. funimass3
485. funimass5
486. funconstss
487. fvimacnvALT
488. elpreima
489. elpreimad
490. fniniseg
491. fncnvima2
492. fniniseg2
493. unpreima
494. inpreima
495. difpreima
496. respreima
497. iinpreima
498. intpreima
499. fimacnv
500. fimacnvinrn
501. fimacnvinrn2
502. fvn0ssdmfun
503. fnopfv
504. fvelrn
505. nelrnfvne
506. fveqdmss
507. fveqressseq
508. fnfvelrn
509. ffvelrn
510. ffvelrni
511. ffvelrnda
512. ffvelrnd
513. rexrn
514. ralrn
515. elrnrexdm
516. elrnrexdmb
517. eldmrexrn
518. eldmrexrnb
519. fvcofneq
520. ralrnmptw
521. rexrnmptw
522. ralrnmpt
523. rexrnmpt
524. f0cli
525. dff2
526. dff3
527. dff4
528. dffo3
529. dffo4
530. dffo5
531. exfo
532. foelrn
533. foco2
534. fmpt
535. f1ompt
536. fmpti
537. fvmptelrn
538. fmptd
539. fmpttd
540. fmpt3d
541. fmptdf
542. ffnfv
543. ffnfvf
544. fnfvrnss
545. frnssb
546. rnmptss
547. fmpt2d
548. ffvresb
549. f1oresrab
550. f1ossf1o
551. fmptco
552. fmptcof
553. fmptcos
554. cofmpt
555. fcompt
556. fcoconst
557. fsn
558. fsn2
559. fsng
560. fsn2g
561. xpsng
562. xpprsng
563. xpsn
564. f1o2sn
565. residpr
566. dfmpt
567. fnasrn
568. idref
569. funiun
570. funopsn
571. funop
572. funopdmsn
573. funsndifnop
574. funsneqopb
575. ressnop0
576. fpr
577. fprg
578. ftpg
579. ftp
580. fnressn
581. funressn
582. fressnfv
583. fvrnressn
584. fvressn
585. fvn0fvelrn
586. fvconst
587. fnsnr
588. fnsnb
589. fmptsn
590. fmptsng
591. fmptsnd
592. fmptap
593. fmptapd
594. fmptpr
595. fvresi
596. fninfp
597. fnelfp
598. fndifnfp
599. fnelnfp
600. fnnfpeq0
601. fvunsn
602. fvsng
603. fvsn
604. fvsnun1
605. fvsnun2
606. fnsnsplit
607. fsnunf
608. fsnunf2
609. fsnunfv
610. fsnunres
611. funresdfunsn
612. fvpr1
613. fvpr2
614. fvpr1g
615. fvpr2g
616. fprb
617. fvtp1
618. fvtp2
619. fvtp3
620. fvtp1g
621. fvtp2g
622. fvtp3g
623. tpres
624. fvconst2g
625. fconst2g
626. fvconst2
627. fconst2
628. fconst5
629. rnmptc
630. rnmptcOLD
631. fnprb
632. fntpb
633. fnpr2g
634. fpr2g
635. fconstfv
636. fconst3
637. fconst4
638. resfunexg
639. resiexd
640. fnex
641. fnexd
642. funex
643. opabex
644. mptexg
645. mptexgf
646. mptex
647. mptexd
648. mptrabex
649. fex
650. fexd
651. mptfvmpt
652. eufnfv
653. funfvima
654. funfvima2
655. funfvima2d
656. fnfvima
657. fnfvimad
658. resfvresima
659. funfvima3
660. rexima
661. ralima
662. fvclss
663. elabrex
664. abrexco
665. imaiun
666. imauni
667. fniunfv
668. funiunfv
669. funiunfvf
670. eluniima
671. elunirn
672. elunirnALT
673. fnunirn
674. dff13
675. dff13f
676. f1veqaeq
677. f1cofveqaeq
678. f1cofveqaeqALT
679. 2f1fvneq
680. f1mpt
681. f1fveq
682. f1elima
683. f1imass
684. f1imaeq
685. f1imapss
686. fpropnf1
687. f1dom3fv3dif
688. f1dom3el3dif
689. dff14a
690. dff14b
691. f12dfv
692. f13dfv
693. dff1o6
694. f1ocnvfv1
695. f1ocnvfv2
696. f1ocnvfv
697. f1ocnvfvb
698. nvof1o
699. nvocnv
700. fsnex
701. f1prex
702. f1ocnvdm
703. f1ocnvfvrneq
704. fcof1
705. fcofo
706. cbvfo
707. cbvexfo
708. cocan1
709. cocan2
710. fcof1oinvd
711. fcof1od
712. 2fcoidinvd
713. fcof1o
714. 2fvcoidd
715. 2fvidf1od
716. 2fvidinvd
717. foeqcnvco
718. f1eqcocnv
719. f1eqcocnvOLD
720. fveqf1o
721. nf1const
722. nf1oconst
723. fliftrel
724. fliftel
725. fliftel1
726. fliftcnv
727. fliftfun
728. fliftfund
729. fliftfuns
730. fliftf
731. fliftval
732. isoeq1
733. isoeq2
734. isoeq3
735. isoeq4
736. isoeq5
737. nfiso
738. isof1o
739. isof1oidb
740. isof1oopb
741. isorel
742. soisores
743. soisoi
744. isoid
745. isocnv
746. isocnv2
747. isocnv3
748. isores2
749. isores1
750. isores3
751. isotr
752. isomin
753. isoini
754. isoini2
755. isofrlem
756. isoselem
757. isofr
758. isose
759. isofr2
760. isopolem
761. isopo
762. isosolem
763. isoso
764. isowe
765. isowe2
766. f1oiso
767. f1oiso2
768. f1owe
769. weniso
770. weisoeq
771. weisoeq2
772. 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. 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
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. offval
11. ofrfval
12. ofval
13. ofrval
14. offn
15. offun
16. offval2f
17. ofmresval
18. fnfvof
19. off
20. ofres
21. offval2
22. ofrfval2
23. ofmpteq
24. ofco
25. offveq
26. offveqb
27. ofc1
28. ofc2
29. ofc12
30. caofref
31. caofinvl
32. caofid0l
33. caofid0r
34. caofid1
35. caofid2
36. caofcom
37. caofrss
38. caofass
39. caoftrn
40. caofdi
41. caofdir
42. 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