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. epelgOLD
5. epeli
6. epel
7. 0sn0ep
8. 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. elrnmptdv
282. elrnmpt2d
283. dfiun3g
284. dfiin3g
285. dfiun3
286. dfiin3
287. riinint
288. relrn0
289. dmrnssfld
290. dmcoss
291. rncoss
292. dmcosseq
293. dmcoeq
294. rncoeq
295. reseq1
296. reseq2
297. reseq1i
298. reseq2i
299. reseq12i
300. reseq1d
301. reseq2d
302. reseq12d
303. nfres
304. csbres
305. res0
306. dfres3
307. opelres
308. brres
309. opelresi
310. brresi
311. opres
312. resieq
313. opelidres
314. resres
315. resundi
316. resundir
317. resindi
318. resindir
319. inres
320. resdifcom
321. resiun1
322. resiun2
323. dmres
324. ssdmres
325. dmresexg
326. resss
327. rescom
328. ssres
329. ssres2
330. relres
331. resabs1
332. resabs1d
333. resabs2
334. residm
335. resima
336. resima2
337. xpssres
338. elinxp
339. elres
340. elsnres
341. relssres
342. dmressnsn
343. eldmressnsn
344. eldmeldmressn
345. resdm
346. resexg
347. resex
348. resindm
349. resdmdfsn
350. resopab
351. iss
352. resopab2
353. resmpt
354. resmpt3
355. resmptf
356. resmptd
357. dfres2
358. mptss
359. elidinxp
360. elidinxpid
361. elrid
362. idinxpres
363. idinxpresid
364. idssxp
365. opabresid
366. mptresid
367. opabresidOLD
368. mptresidOLD
369. dmresi
370. restidsing
371. iresn0n0
372. imaeq1
373. imaeq2
374. imaeq1i
375. imaeq2i
376. imaeq1d
377. imaeq2d
378. imaeq12d
379. dfima2
380. dfima3
381. elimag
382. elima
383. elima2
384. elima3
385. nfima
386. nfimad
387. imadmrn
388. imassrn
389. mptima
390. imai
391. rnresi
392. resiima
393. ima0
394. 0ima
395. csbima12
396. imadisj
397. cnvimass
398. cnvimarndm
399. imasng
400. relimasn
401. elrelimasn
402. elimasn
403. elimasng
404. elimasni
405. args
406. eliniseg
407. epini
408. iniseg
409. inisegn0
410. dffr3
411. dfse2
412. imass1
413. imass2
414. ndmima
415. relcnv
416. relbrcnvg
417. eliniseg2
418. relbrcnv
419. cotrg
420. cotr
421. idrefALT
422. cnvsym
423. intasym
424. asymref
425. asymref2
426. intirr
427. brcodir
428. codir
429. qfto
430. xpidtr
431. trin2
432. poirr2
433. trinxp
434. soirri
435. sotri
436. son2lpi
437. sotri2
438. sotri3
439. poleloe
440. poltletr
441. somin1
442. somincom
443. somin2
444. soltmin
445. cnvopab
446. mptcnv
447. cnv0
448. cnvi
449. cnvun
450. cnvdif
451. cnvin
452. rnun
453. rnin
454. rniun
455. rnuni
456. imaundi
457. imaundir
458. dminss
459. imainss
460. inimass
461. inimasn
462. cnvxp
463. xp0
464. xpnz
465. xpeq0
466. xpdisj1
467. xpdisj2
468. xpsndisj
469. difxp
470. difxp1
471. difxp2
472. djudisj
473. xpdifid
474. resdisj
475. rnxp
476. dmxpss
477. rnxpss
478. rnxpid
479. ssxpb
480. xp11
481. xpcan
482. xpcan2
483. ssrnres
484. rninxp
485. dminxp
486. imainrect
487. xpima
488. xpima1
489. xpima2
490. xpimasn
491. sossfld
492. sofld
493. cnvcnv3
494. dfrel2
495. dfrel4v
496. dfrel4
497. cnvcnv
498. cnvcnv2
499. cnvcnvss
500. cnvrescnv
501. cnveqb
502. cnveq0
503. dfrel3
504. elid
505. dmresv
506. rnresv
507. dfrn4
508. csbrn
509. rescnvcnv
510. cnvcnvres
511. imacnvcnv
512. dmsnn0
513. rnsnn0
514. dmsn0
515. cnvsn0
516. dmsn0el
517. relsn2
518. dmsnopg
519. dmsnopss
520. dmpropg
521. dmsnop
522. dmprop
523. dmtpop
524. cnvcnvsn
525. dmsnsnsn
526. rnsnopg
527. rnpropg
528. cnvsng
529. rnsnop
530. op1sta
531. cnvsn
532. op2ndb
533. op2nda
534. opswap
535. cnvresima
536. resdm2
537. resdmres
538. resresdm
539. imadmres
540. mptpreima
541. mptiniseg
542. dmmpt
543. dmmptss
544. dmmptg
545. relco
546. dfco2
547. dfco2a
548. coundi
549. coundir
550. cores
551. resco
552. imaco
553. rnco
554. rnco2
555. dmco
556. coeq0
557. coiun
558. cocnvcnv1
559. cocnvcnv2
560. cores2
561. co02
562. co01
563. coi1
564. coi2
565. coires1
566. coass
567. relcnvtrg
568. relcnvtr
569. relssdmrn
570. cnvssrndm
571. cossxp
572. relrelss
573. unielrel
574. relfld
575. relresfld
576. relcoi2
577. relcoi1
578. unidmrn
579. relcnvfld
580. dfdm2
581. unixp
582. unixp0
583. unixpid
584. ressn
585. cnviin
586. cnvpo
587. cnvso
588. xpco
589. xpcoid
590. elsnxp
591. reu3op
592. reuop
593. opreu2reurex
594. 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
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. funssres
51. fun2ssres
52. funun
53. fununmo
54. fununfun
55. fundif
56. funcnvsn
57. funsng
58. fnsng
59. funsn
60. funprg
61. funtpg
62. funpr
63. funtp
64. fnsn
65. fnprg
66. fntpg
67. fntp
68. funcnvpr
69. funcnvtp
70. funcnvqp
71. fun0
72. funcnv0
73. funcnvcnv
74. funcnv2
75. funcnv
76. funcnv3
77. fun2cnv
78. svrelfun
79. fncnv
80. fun11
81. fununi
82. funin
83. funres11
84. funcnvres
85. cnvresid
86. funcnvres2
87. funimacnv
88. funimass1
89. funimass2
90. imadif
91. imain
92. funimaexg
93. funimaex
94. isarep1
95. isarep2
96. fneq1
97. fneq2
98. fneq1d
99. fneq2d
100. fneq12d
101. fneq12
102. fneq1i
103. fneq2i
104. nffn
105. fnfun
106. fnrel
107. fndm
108. fndmd
109. funfni
110. fndmu
111. fnbr
112. fnop
113. fneu
114. fneu2
115. fnun
116. fnunsn
117. fnco
118. fnresdm
119. fnresdisj
120. 2elresin
121. fnssresb
122. fnssres
123. fnssresd
124. fnresin1
125. fnresin2
126. fnres
127. idfn
128. fnresi
129. fnresiOLD
130. fnima
131. fn0
132. fnimadisj
133. fnimaeq0
134. dfmpt3
135. mptfnf
136. fnmptf
137. fnopabg
138. fnopab
139. mptfng
140. fnmpt
141. fnmptd
142. mpt0
143. fnmpti
144. dmmpti
145. dmmptd
146. mptun
147. feq1
148. feq2
149. feq3
150. feq23
151. feq1d
152. feq2d
153. feq3d
154. feq12d
155. feq123d
156. feq123
157. feq1i
158. feq2i
159. feq12i
160. feq23i
161. feq23d
162. nff
163. sbcfng
164. sbcfg
165. elimf
166. ffn
167. ffnd
168. dffn2
169. ffun
170. ffund
171. frel
172. frn
173. frnd
174. fdm
175. fdmd
176. fdmi
177. dffn3
178. ffrn
179. fss
180. fssd
181. fssdmd
182. fssdm
183. fco
184. fcod
185. fco2
186. fssxp
187. funssxp
188. ffdm
189. ffdmd
190. fdmrn
191. opelf
192. fun
193. fun2
194. fun2d
195. fnfco
196. fssres
197. fssresd
198. fssres2
199. fresin
200. resasplit
201. fresaun
202. fresaunres2
203. fresaunres1
204. fcoi1
205. fcoi2
206. feu
207. fimass
208. fcnvres
209. fimacnvdisj
210. fint
211. fin
212. f0
213. f00
214. f0bi
215. f0dom0
216. f0rn0
217. fconst
218. fconstg
219. fnconstg
220. fconst6g
221. fconst6
222. f1eq1
223. f1eq2
224. f1eq3
225. nff1
226. dff12
227. f1f
228. f1fn
229. f1fun
230. f1rel
231. f1dm
232. f1ss
233. f1ssr
234. f1ssres
235. f1resf1
236. f1cnvcnv
237. f1co
238. foeq1
239. foeq2
240. foeq3
241. nffo
242. fof
243. fofun
244. fofn
245. forn
246. dffo2
247. foima
248. dffn4
249. funforn
250. fodmrnu
251. fimadmfo
252. fores
253. fimadmfoALT
254. foco
255. foconst
256. f1oeq1
257. f1oeq2
258. f1oeq3
259. f1oeq23
260. f1eq123d
261. foeq123d
262. f1oeq123d
263. f1oeq2d
264. f1oeq3d
265. nff1o
266. f1of1
267. f1of
268. f1ofn
269. f1ofun
270. f1orel
271. f1odm
272. dff1o2
273. dff1o3
274. f1ofo
275. dff1o4
276. dff1o5
277. f1orn
278. f1f1orn
279. f1ocnv
280. f1ocnvb
281. f1ores
282. f1orescnv
283. f1imacnv
284. foimacnv
285. foun
286. f1oun
287. resdif
288. resin
289. f1oco
290. f1cnv
291. funcocnv2
292. fococnv2
293. f1ococnv2
294. f1cocnv2
295. f1ococnv1
296. f1cocnv1
297. funcoeqres
298. f1ssf1
299. f10
300. f10d
301. f1o00
302. fo00
303. f1o0
304. f1oi
305. f1ovi
306. f1osn
307. f1osng
308. f1sng
309. fsnd
310. f1oprswap
311. f1oprg
312. tz6.12-2
313. fveu
314. brprcneu
315. fvprc
316. rnfvprc
317. fv2
318. dffv3
319. dffv4
320. elfv
321. fveq1
322. fveq2
323. fveq1i
324. fveq1d
325. fveq2i
326. fveq2d
327. 2fveq3
328. fveq12i
329. fveq12d
330. fveqeq2d
331. fveqeq2
332. nffv
333. nffvmpt1
334. nffvd
335. fvex
336. fvexi
337. fvexd
338. fvif
339. iffv
340. fv3
341. fvres
342. fvresd
343. funssfv
344. tz6.12-1
345. tz6.12
346. tz6.12f
347. tz6.12c
348. tz6.12i
349. fvbr0
350. fvrn0
351. fvssunirn
352. ndmfv
353. ndmfvrcl
354. elfvdm
355. elfvex
356. elfvexd
357. eliman0
358. nfvres
359. nfunsn
360. fvfundmfvn0
361. 0fv
362. fv2prc
363. elfv2ex
364. fveqres
365. csbfv12
366. csbfv2g
367. csbfv
368. funbrfv
369. funopfv
370. fnbrfvb
371. fnopfvb
372. funbrfvb
373. funopfvb
374. fnbrfvb2
375. funbrfv2b
376. dffn5
377. fnrnfv
378. fvelrnb
379. foelrni
380. dfimafn
381. dfimafn2
382. funimass4
383. fvelima
384. fvelimad
385. feqmptd
386. feqresmpt
387. feqmptdf
388. dffn5f
389. fvelimab
390. fvelimabd
391. unima
392. fvi
393. fviss
394. fniinfv
395. fnsnfv
396. opabiotafun
397. opabiotadm
398. opabiota
399. fnimapr
400. ssimaex
401. ssimaexg
402. funfv
403. funfv2
404. funfv2f
405. fvun
406. fvun1
407. fvun2
408. dffv2
409. dmfco
410. fvco2
411. fvco
412. fvco3
413. fvco3d
414. fvco4i
415. fvopab3g
416. fvopab3ig
417. brfvopabrbr
418. fvmptg
419. fvmpti
420. fvmpt
421. fvmpt2f
422. fvtresfn
423. fvmpts
424. fvmpt3
425. fvmpt3i
426. fvmptdf
427. fvmptd
428. fvmptd2
429. mptrcl
430. fvmpt2i
431. fvmpt2
432. fvmptss
433. fvmpt2d
434. fvmptex
435. fvmptd3f
436. fvmptd2f
437. fvmptdv
438. fvmptdv2
439. mpteqb
440. fvmptt
441. fvmptf
442. fvmptnf
443. fvmptd3
444. fvmptn
445. fvmptss2
446. elfvmptrab1w
447. elfvmptrab1
448. elfvmptrab
449. fvopab4ndm
450. fvmptndm
451. fvmptrabfv
452. fvopab5
453. fvopab6
454. eqfnfv
455. eqfnfv2
456. eqfnfv3
457. eqfnfvd
458. eqfnfv2f
459. eqfunfv
460. fvreseq0
461. fvreseq1
462. fvreseq
463. fnmptfvd
464. fndmdif
465. fndmdifcom
466. fndmdifeq0
467. fndmin
468. fneqeql
469. fneqeql2
470. fnreseql
471. chfnrn
472. funfvop
473. funfvbrb
474. fvimacnvi
475. fvimacnv
476. funimass3
477. funimass5
478. funconstss
479. fvimacnvALT
480. elpreima
481. elpreimad
482. fniniseg
483. fncnvima2
484. fniniseg2
485. unpreima
486. inpreima
487. difpreima
488. respreima
489. iinpreima
490. intpreima
491. fimacnv
492. fimacnvinrn
493. fimacnvinrn2
494. fvn0ssdmfun
495. fnopfv
496. fvelrn
497. nelrnfvne
498. fveqdmss
499. fveqressseq
500. fnfvelrn
501. ffvelrn
502. ffvelrni
503. ffvelrnda
504. ffvelrnd
505. rexrn
506. ralrn
507. elrnrexdm
508. elrnrexdmb
509. eldmrexrn
510. eldmrexrnb
511. fvcofneq
512. ralrnmptw
513. rexrnmptw
514. ralrnmpt
515. rexrnmpt
516. f0cli
517. dff2
518. dff3
519. dff4
520. dffo3
521. dffo4
522. dffo5
523. exfo
524. foelrn
525. foco2
526. fmpt
527. f1ompt
528. fmpti
529. fvmptelrn
530. fmptd
531. fmpttd
532. fmpt3d
533. fmptdf
534. ffnfv
535. ffnfvf
536. fnfvrnss
537. frnssb
538. rnmptss
539. fmpt2d
540. ffvresb
541. f1oresrab
542. f1ossf1o
543. fmptco
544. fmptcof
545. fmptcos
546. cofmpt
547. fcompt
548. fcoconst
549. fsn
550. fsn2
551. fsng
552. fsn2g
553. xpsng
554. xpprsng
555. xpsn
556. f1o2sn
557. residpr
558. dfmpt
559. fnasrn
560. idref
561. funiun
562. funopsn
563. funop
564. funopdmsn
565. funsndifnop
566. funsneqopb
567. ressnop0
568. fpr
569. fprg
570. ftpg
571. ftp
572. fnressn
573. funressn
574. fressnfv
575. fvrnressn
576. fvressn
577. fvn0fvelrn
578. fvconst
579. fnsnr
580. fnsnb
581. fmptsn
582. fmptsng
583. fmptsnd
584. fmptap
585. fmptapd
586. fmptpr
587. fvresi
588. fninfp
589. fnelfp
590. fndifnfp
591. fnelnfp
592. fnnfpeq0
593. fvunsn
594. fvsng
595. fvsn
596. fvsnun1
597. fvsnun2
598. fnsnsplit
599. fsnunf
600. fsnunf2
601. fsnunfv
602. fsnunres
603. funresdfunsn
604. fvpr1
605. fvpr2
606. fvpr1g
607. fvpr2g
608. fprb
609. fvtp1
610. fvtp2
611. fvtp3
612. fvtp1g
613. fvtp2g
614. fvtp3g
615. tpres
616. fvconst2g
617. fconst2g
618. fvconst2
619. fconst2
620. fconst5
621. rnmptc
622. rnmptcOLD
623. fnprb
624. fntpb
625. fnpr2g
626. fpr2g
627. fconstfv
628. fconst3
629. fconst4
630. resfunexg
631. resiexd
632. fnex
633. fnexd
634. funex
635. opabex
636. mptexg
637. mptexgf
638. mptex
639. mptexd
640. mptrabex
641. fex
642. mptfvmpt
643. eufnfv
644. funfvima
645. funfvima2
646. funfvima2d
647. fnfvima
648. fnfvimad
649. resfvresima
650. funfvima3
651. rexima
652. ralima
653. fvclss
654. elabrex
655. abrexco
656. imaiun
657. imauni
658. fniunfv
659. funiunfv
660. funiunfvf
661. eluniima
662. elunirn
663. elunirnALT
664. fnunirn
665. dff13
666. dff13f
667. f1veqaeq
668. f1cofveqaeq
669. f1cofveqaeqALT
670. 2f1fvneq
671. f1mpt
672. f1fveq
673. f1elima
674. f1imass
675. f1imaeq
676. f1imapss
677. fpropnf1
678. f1dom3fv3dif
679. f1dom3el3dif
680. dff14a
681. dff14b
682. f12dfv
683. f13dfv
684. dff1o6
685. f1ocnvfv1
686. f1ocnvfv2
687. f1ocnvfv
688. f1ocnvfvb
689. nvof1o
690. nvocnv
691. fsnex
692. f1prex
693. f1ocnvdm
694. f1ocnvfvrneq
695. fcof1
696. fcofo
697. cbvfo
698. cbvexfo
699. cocan1
700. cocan2
701. fcof1oinvd
702. fcof1od
703. 2fcoidinvd
704. fcof1o
705. 2fvcoidd
706. 2fvidf1od
707. 2fvidinvd
708. foeqcnvco
709. f1eqcocnv
710. fveqf1o
711. nf1const
712. nf1oconst
713. fliftrel
714. fliftel
715. fliftel1
716. fliftcnv
717. fliftfun
718. fliftfund
719. fliftfuns
720. fliftf
721. fliftval
722. isoeq1
723. isoeq2
724. isoeq3
725. isoeq4
726. isoeq5
727. nfiso
728. isof1o
729. isof1oidb
730. isof1oopb
731. isorel
732. soisores
733. soisoi
734. isoid
735. isocnv
736. isocnv2
737. isocnv3
738. isores2
739. isores1
740. isores3
741. isotr
742. isomin
743. isoini
744. isoini2
745. isofrlem
746. isoselem
747. isofr
748. isose
749. isofr2
750. isopolem
751. isopo
752. isosolem
753. isoso
754. isowe
755. isowe2
756. f1oiso
757. f1oiso2
758. f1owe
759. weniso
760. weisoeq
761. weisoeq2
762. 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. fnoprab
123. ffnov
124. fovcl
125. eqfnov
126. eqfnov2
127. fnov
128. mpo2eqb
129. rnmpo
130. reldmmpo
131. elrnmpog
132. elrnmpo
133. elrnmpores
134. ralrnmpo
135. rexrnmpo
136. ovid
137. ovidig
138. ovidi
139. ov
140. ovigg
141. ovig
142. ovmpt4g
143. ovmpos
144. ov2gf
145. ovmpodxf
146. ovmpodx
147. ovmpod
148. ovmpox
149. ovmpoga
150. ovmpoa
151. ovmpodf
152. ovmpodv
153. ovmpodv2
154. ovmpog
155. ovmpo
156. ov3
157. ov6g
158. ovg
159. ovres
160. ovresd
161. oprres
162. oprssov
163. fovrn
164. fovrnda
165. fovrnd
166. fnrnov
167. foov
168. fnovrn
169. ovelrn
170. funimassov
171. ovelimab
172. ovima0
173. ovconst2
174. oprssdm
175. nssdmovg
176. ndmovg
177. ndmov
178. ndmovcl
179. ndmovrcl
180. ndmovcom
181. ndmovass
182. ndmovdistr
183. ndmovord
184. ndmovordi
185. 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. offval2f
16. ofmresval
17. fnfvof
18. off
19. ofres
20. offval2
21. ofrfval2
22. ofmpteq
23. ofco
24. offveq
25. offveqb
26. ofc1
27. ofc2
28. ofc12
29. caofref
30. caofinvl
31. caofid0l
32. caofid0r
33. caofid1
34. caofid2
35. caofcom
36. caofrss
37. caofass
38. caoftrn
39. caofdi
40. caofdir
41. 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