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. 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. elrn2
212. elrn
213. ssrelrn
214. dfdm4
215. dfdmf
216. csbdm
217. eldmg
218. eldm2g
219. eldm
220. eldm2
221. dmss
222. dmeq
223. dmeqi
224. dmeqd
225. opeldmd
226. opeldm
227. breldm
228. breldmg
229. dmun
230. dmin
231. breldmd
232. dmiun
233. dmuni
234. dmopab
235. dmopabelb
236. dmopab2rex
237. dmopabss
238. dmopab3
239. opabssxpd
240. dm0
241. dmi
242. dmv
243. dmep
244. domepOLD
245. dm0rn0
246. rn0
247. rnep
248. reldm0
249. dmxp
250. dmxpid
251. dmxpin
252. xpid11
253. dmcnvcnv
254. rncnvcnv
255. elreldm
256. rneq
257. rneqi
258. rneqd
259. rnss
260. rnssi
261. brelrng
262. brelrn
263. opelrn
264. releldm
265. relelrn
266. releldmb
267. relelrnb
268. releldmi
269. relelrni
270. dfrnf
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. resdmss
544. resdifdi
545. resdifdir
546. mptpreima
547. mptiniseg
548. dmmpt
549. dmmptss
550. dmmptg
551. rnmpt0f
552. rnmptn0
553. relco
554. dfco2
555. dfco2a
556. coundi
557. coundir
558. cores
559. resco
560. imaco
561. rnco
562. rnco2
563. dmco
564. coeq0
565. coiun
566. cocnvcnv1
567. cocnvcnv2
568. cores2
569. co02
570. co01
571. coi1
572. coi2
573. coires1
574. coass
575. relcnvtrg
576. relcnvtr
577. relssdmrn
578. resssxp
579. cnvssrndm
580. cossxp
581. relrelss
582. unielrel
583. relfld
584. relresfld
585. relcoi2
586. relcoi1
587. unidmrn
588. relcnvfld
589. dfdm2
590. unixp
591. unixp0
592. unixpid
593. ressn
594. cnviin
595. cnvpo
596. cnvso
597. xpco
598. xpcoid
599. elsnxp
600. reu3op
601. reuop
602. opreu2reurex
603. 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. 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. fnunop
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. f1oeq1d
270. f1oeq2d
271. f1oeq3d
272. nff1o
273. f1of1
274. f1of
275. f1ofn
276. f1ofun
277. f1orel
278. f1odm
279. dff1o2
280. dff1o3
281. f1ofo
282. dff1o4
283. dff1o5
284. f1orn
285. f1f1orn
286. f1ocnv
287. f1ocnvb
288. f1ores
289. f1orescnv
290. f1imacnv
291. foimacnv
292. foun
293. f1oun
294. resdif
295. resin
296. f1oco
297. f1cnv
298. funcocnv2
299. fococnv2
300. f1ococnv2
301. f1cocnv2
302. f1ococnv1
303. f1cocnv1
304. funcoeqres
305. f1ssf1
306. f10
307. f10d
308. f1o00
309. fo00
310. f1o0
311. f1oi
312. f1ovi
313. f1osn
314. f1osng
315. f1sng
316. fsnd
317. f1oprswap
318. f1oprg
319. tz6.12-2
320. fveu
321. brprcneu
322. fvprc
323. fvprcALT
324. rnfvprc
325. fv2
326. dffv3
327. dffv4
328. elfv
329. fveq1
330. fveq2
331. fveq1i
332. fveq1d
333. fveq2i
334. fveq2d
335. 2fveq3
336. fveq12i
337. fveq12d
338. fveqeq2d
339. fveqeq2
340. nffv
341. nffvmpt1
342. nffvd
343. fvex
344. fvexi
345. fvexd
346. fvif
347. iffv
348. fv3
349. fvres
350. fvresd
351. funssfv
352. tz6.12-1
353. tz6.12
354. tz6.12f
355. tz6.12c
356. tz6.12i
357. fvbr0
358. fvrn0
359. fvssunirn
360. ndmfv
361. ndmfvrcl
362. elfvdm
363. elfvex
364. elfvexd
365. eliman0
366. nfvres
367. nfunsn
368. fvfundmfvn0
369. 0fv
370. fv2prc
371. elfv2ex
372. fveqres
373. csbfv12
374. csbfv2g
375. csbfv
376. funbrfv
377. funopfv
378. fnbrfvb
379. fnopfvb
380. funbrfvb
381. funopfvb
382. fnbrfvb2
383. funbrfv2b
384. dffn5
385. fnrnfv
386. fvelrnb
387. foelrni
388. dfimafn
389. dfimafn2
390. funimass4
391. fvelima
392. fvelimad
393. feqmptd
394. feqresmpt
395. feqmptdf
396. dffn5f
397. fvelimab
398. fvelimabd
399. unima
400. fvi
401. fviss
402. fniinfv
403. fnsnfv
404. fnsnfvOLD
405. opabiotafun
406. opabiotadm
407. opabiota
408. fnimapr
409. ssimaex
410. ssimaexg
411. funfv
412. funfv2
413. funfv2f
414. fvun
415. fvun1
416. fvun2
417. fvun1d
418. fvun2d
419. dffv2
420. dmfco
421. fvco2
422. fvco
423. fvco3
424. fvco3d
425. fvco4i
426. fvopab3g
427. fvopab3ig
428. brfvopabrbr
429. fvmptg
430. fvmpti
431. fvmpt
432. fvmpt2f
433. fvtresfn
434. fvmpts
435. fvmpt3
436. fvmpt3i
437. fvmptdf
438. fvmptd
439. fvmptd2
440. mptrcl
441. fvmpt2i
442. fvmpt2
443. fvmptss
444. fvmpt2d
445. fvmptex
446. fvmptd3f
447. fvmptd2f
448. fvmptdv
449. fvmptdv2
450. mpteqb
451. fvmptt
452. fvmptf
453. fvmptnf
454. fvmptd3
455. fvmptn
456. fvmptss2
457. elfvmptrab1w
458. elfvmptrab1
459. elfvmptrab
460. fvopab4ndm
461. fvmptndm
462. fvmptrabfv
463. fvopab5
464. fvopab6
465. eqfnfv
466. eqfnfv2
467. eqfnfv3
468. eqfnfvd
469. eqfnfv2f
470. eqfunfv
471. fvreseq0
472. fvreseq1
473. fvreseq
474. fnmptfvd
475. fndmdif
476. fndmdifcom
477. fndmdifeq0
478. fndmin
479. fneqeql
480. fneqeql2
481. fnreseql
482. chfnrn
483. funfvop
484. funfvbrb
485. fvimacnvi
486. fvimacnv
487. funimass3
488. funimass5
489. funconstss
490. fvimacnvALT
491. elpreima
492. elpreimad
493. fniniseg
494. fncnvima2
495. fniniseg2
496. unpreima
497. inpreima
498. difpreima
499. respreima
500. iinpreima
501. intpreima
502. fimacnv
503. fimacnvinrn
504. fimacnvinrn2
505. fvn0ssdmfun
506. fnopfv
507. fvelrn
508. nelrnfvne
509. fveqdmss
510. fveqressseq
511. fnfvelrn
512. ffvelrn
513. ffvelrni
514. ffvelrnda
515. ffvelrnd
516. rexrn
517. ralrn
518. elrnrexdm
519. elrnrexdmb
520. eldmrexrn
521. eldmrexrnb
522. fvcofneq
523. ralrnmptw
524. rexrnmptw
525. ralrnmpt
526. rexrnmpt
527. f0cli
528. dff2
529. dff3
530. dff4
531. dffo3
532. dffo4
533. dffo5
534. exfo
535. foelrn
536. foco2
537. fmpt
538. f1ompt
539. fmpti
540. fvmptelrn
541. fmptd
542. fmpttd
543. fmpt3d
544. fmptdf
545. ffnfv
546. ffnfvf
547. fnfvrnss
548. frnssb
549. rnmptss
550. fmpt2d
551. ffvresb
552. f1oresrab
553. f1ossf1o
554. fmptco
555. fmptcof
556. fmptcos
557. cofmpt
558. fcompt
559. fcoconst
560. fsn
561. fsn2
562. fsng
563. fsn2g
564. xpsng
565. xpprsng
566. xpsn
567. f1o2sn
568. residpr
569. dfmpt
570. fnasrn
571. idref
572. funiun
573. funopsn
574. funop
575. funopdmsn
576. funsndifnop
577. funsneqopb
578. ressnop0
579. fpr
580. fprg
581. ftpg
582. ftp
583. fnressn
584. funressn
585. fressnfv
586. fvrnressn
587. fvressn
588. fvn0fvelrn
589. fvconst
590. fnsnr
591. fnsnb
592. fmptsn
593. fmptsng
594. fmptsnd
595. fmptap
596. fmptapd
597. fmptpr
598. fvresi
599. fninfp
600. fnelfp
601. fndifnfp
602. fnelnfp
603. fnnfpeq0
604. fvunsn
605. fvsng
606. fvsn
607. fvsnun1
608. fvsnun2
609. fnsnsplit
610. fsnunf
611. fsnunf2
612. fsnunfv
613. fsnunres
614. funresdfunsn
615. fvpr1
616. fvpr2
617. fvpr1g
618. fvpr2g
619. fprb
620. fvtp1
621. fvtp2
622. fvtp3
623. fvtp1g
624. fvtp2g
625. fvtp3g
626. tpres
627. fvconst2g
628. fconst2g
629. fvconst2
630. fconst2
631. fconst5
632. rnmptc
633. rnmptcOLD
634. fnprb
635. fntpb
636. fnpr2g
637. fpr2g
638. fconstfv
639. fconst3
640. fconst4
641. resfunexg
642. resiexd
643. fnex
644. fnexd
645. funex
646. opabex
647. mptexg
648. mptexgf
649. mptex
650. mptexd
651. mptrabex
652. fex
653. fexd
654. mptfvmpt
655. eufnfv
656. funfvima
657. funfvima2
658. funfvima2d
659. fnfvima
660. fnfvimad
661. resfvresima
662. funfvima3
663. rexima
664. ralima
665. fvclss
666. elabrex
667. abrexco
668. imaiun
669. imauni
670. fniunfv
671. funiunfv
672. funiunfvf
673. eluniima
674. elunirn
675. elunirnALT
676. fnunirn
677. dff13
678. dff13f
679. f1veqaeq
680. f1cofveqaeq
681. f1cofveqaeqALT
682. 2f1fvneq
683. f1mpt
684. f1fveq
685. f1elima
686. f1imass
687. f1imaeq
688. f1imapss
689. fpropnf1
690. f1dom3fv3dif
691. f1dom3el3dif
692. dff14a
693. dff14b
694. f12dfv
695. f13dfv
696. dff1o6
697. f1ocnvfv1
698. f1ocnvfv2
699. f1ocnvfv
700. f1ocnvfvb
701. nvof1o
702. nvocnv
703. fsnex
704. f1prex
705. f1ocnvdm
706. f1ocnvfvrneq
707. fcof1
708. fcofo
709. cbvfo
710. cbvexfo
711. cocan1
712. cocan2
713. fcof1oinvd
714. fcof1od
715. 2fcoidinvd
716. fcof1o
717. 2fvcoidd
718. 2fvidf1od
719. 2fvidinvd
720. foeqcnvco
721. f1eqcocnv
722. f1eqcocnvOLD
723. fveqf1o
724. nf1const
725. nf1oconst
726. f1ofvswap
727. fliftrel
728. fliftel
729. fliftel1
730. fliftcnv
731. fliftfun
732. fliftfund
733. fliftfuns
734. fliftf
735. fliftval
736. isoeq1
737. isoeq2
738. isoeq3
739. isoeq4
740. isoeq5
741. nfiso
742. isof1o
743. isof1oidb
744. isof1oopb
745. isorel
746. soisores
747. soisoi
748. isoid
749. isocnv
750. isocnv2
751. isocnv3
752. isores2
753. isores1
754. isores3
755. isotr
756. isomin
757. isoini
758. isoini2
759. isofrlem
760. isoselem
761. isofr
762. isose
763. isofr2
764. isopolem
765. isopo
766. isosolem
767. isoso
768. isowe
769. isowe2
770. f1oiso
771. f1oiso2
772. f1owe
773. weniso
774. weisoeq
775. weisoeq2
776. 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. 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