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