Metamath Proof Explorer


Table of Contents - 2.3. ZF Set Theory - add the Axiom of Power Sets

  1. 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
  2. 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
  3. 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
  4. 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
  5. Power class of union and intersection
    1. pwin
    2. pwunssOLD
    3. pwssun
    4. pwundifOLD
    5. pwun
  6. The identity relation
    1. cid
    2. df-id
    3. dfid4
    4. dfid3
    5. dfid2
  7. The membership relation (or epsilon relation)
    1. cep
    2. df-eprel
    3. epelg
    4. epelgOLD
    5. epeli
    6. epel
    7. 0sn0ep
    8. epn0
  8. 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
  9. 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
  10. 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
  11. 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
  12. 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
  13. 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
  14. 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
  15. 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. fdmOLD
    176. fdmd
    177. fdmi
    178. dffn3
    179. ffrn
    180. fss
    181. fssd
    182. fssdmd
    183. fssdm
    184. fco
    185. fcod
    186. fco2
    187. fssxp
    188. funssxp
    189. ffdm
    190. ffdmd
    191. fdmrn
    192. opelf
    193. fun
    194. fun2
    195. fun2d
    196. fnfco
    197. fssres
    198. fssresd
    199. fssres2
    200. fresin
    201. resasplit
    202. fresaun
    203. fresaunres2
    204. fresaunres1
    205. fcoi1
    206. fcoi2
    207. feu
    208. fimass
    209. fcnvres
    210. fimacnvdisj
    211. fint
    212. fin
    213. f0
    214. f00
    215. f0bi
    216. f0dom0
    217. f0rn0
    218. fconst
    219. fconstg
    220. fnconstg
    221. fconst6g
    222. fconst6
    223. f1eq1
    224. f1eq2
    225. f1eq3
    226. nff1
    227. dff12
    228. f1f
    229. f1fn
    230. f1fun
    231. f1rel
    232. f1dm
    233. f1dmOLD
    234. f1ss
    235. f1ssr
    236. f1ssres
    237. f1resf1
    238. f1cnvcnv
    239. f1co
    240. foeq1
    241. foeq2
    242. foeq3
    243. nffo
    244. fof
    245. fofun
    246. fofn
    247. forn
    248. dffo2
    249. foima
    250. dffn4
    251. funforn
    252. fodmrnu
    253. fimadmfo
    254. fores
    255. fimadmfoALT
    256. foco
    257. foconst
    258. f1oeq1
    259. f1oeq2
    260. f1oeq3
    261. f1oeq23
    262. f1eq123d
    263. foeq123d
    264. f1oeq123d
    265. f1oeq2d
    266. f1oeq3d
    267. nff1o
    268. f1of1
    269. f1of
    270. f1ofn
    271. f1ofun
    272. f1orel
    273. f1odm
    274. dff1o2
    275. dff1o3
    276. f1ofo
    277. dff1o4
    278. dff1o5
    279. f1orn
    280. f1f1orn
    281. f1ocnv
    282. f1ocnvb
    283. f1ores
    284. f1orescnv
    285. f1imacnv
    286. foimacnv
    287. foun
    288. f1oun
    289. resdif
    290. resin
    291. f1oco
    292. f1cnv
    293. funcocnv2
    294. fococnv2
    295. f1ococnv2
    296. f1cocnv2
    297. f1ococnv1
    298. f1cocnv1
    299. funcoeqres
    300. f1ssf1
    301. f10
    302. f10d
    303. f1o00
    304. fo00
    305. f1o0
    306. f1oi
    307. f1ovi
    308. f1osn
    309. f1osng
    310. f1sng
    311. fsnd
    312. f1oprswap
    313. f1oprg
    314. tz6.12-2
    315. fveu
    316. brprcneu
    317. fvprc
    318. rnfvprc
    319. fv2
    320. dffv3
    321. dffv4
    322. elfv
    323. fveq1
    324. fveq2
    325. fveq1i
    326. fveq1d
    327. fveq2i
    328. fveq2d
    329. 2fveq3
    330. fveq12i
    331. fveq12d
    332. fveqeq2d
    333. fveqeq2
    334. nffv
    335. nffvmpt1
    336. nffvd
    337. fvex
    338. fvexi
    339. fvexd
    340. fvif
    341. iffv
    342. fv3
    343. fvres
    344. fvresd
    345. funssfv
    346. tz6.12-1
    347. tz6.12
    348. tz6.12f
    349. tz6.12c
    350. tz6.12i
    351. fvbr0
    352. fvrn0
    353. fvssunirn
    354. ndmfv
    355. ndmfvrcl
    356. elfvdm
    357. elfvex
    358. elfvexd
    359. eliman0
    360. nfvres
    361. nfunsn
    362. fvfundmfvn0
    363. 0fv
    364. fv2prc
    365. elfv2ex
    366. fveqres
    367. csbfv12
    368. csbfv2g
    369. csbfv
    370. funbrfv
    371. funopfv
    372. fnbrfvb
    373. fnopfvb
    374. funbrfvb
    375. funopfvb
    376. fnbrfvb2
    377. funbrfv2b
    378. dffn5
    379. fnrnfv
    380. fvelrnb
    381. foelrni
    382. dfimafn
    383. dfimafn2
    384. funimass4
    385. fvelima
    386. fvelimad
    387. feqmptd
    388. feqresmpt
    389. feqmptdf
    390. dffn5f
    391. fvelimab
    392. fvelimabd
    393. unima
    394. fvi
    395. fviss
    396. fniinfv
    397. fnsnfv
    398. opabiotafun
    399. opabiotadm
    400. opabiota
    401. fnimapr
    402. ssimaex
    403. ssimaexg
    404. funfv
    405. funfv2
    406. funfv2f
    407. fvun
    408. fvun1
    409. fvun2
    410. dffv2
    411. dmfco
    412. fvco2
    413. fvco
    414. fvco3
    415. fvco3d
    416. fvco4i
    417. fvopab3g
    418. fvopab3ig
    419. brfvopabrbr
    420. fvmptg
    421. fvmpti
    422. fvmpt
    423. fvmpt2f
    424. fvtresfn
    425. fvmpts
    426. fvmpt3
    427. fvmpt3i
    428. fvmptdf
    429. fvmptd
    430. fvmptd2
    431. mptrcl
    432. fvmpt2i
    433. fvmpt2
    434. fvmptss
    435. fvmpt2d
    436. fvmptex
    437. fvmptd3f
    438. fvmptd2f
    439. fvmptdv
    440. fvmptdv2
    441. mpteqb
    442. fvmptt
    443. fvmptf
    444. fvmptnf
    445. fvmptd3
    446. fvmptn
    447. fvmptss2
    448. elfvmptrab1w
    449. elfvmptrab1
    450. elfvmptrab
    451. fvopab4ndm
    452. fvmptndm
    453. fvmptrabfv
    454. fvopab5
    455. fvopab6
    456. eqfnfv
    457. eqfnfv2
    458. eqfnfv3
    459. eqfnfvd
    460. eqfnfv2f
    461. eqfunfv
    462. fvreseq0
    463. fvreseq1
    464. fvreseq
    465. fnmptfvd
    466. fndmdif
    467. fndmdifcom
    468. fndmdifeq0
    469. fndmin
    470. fneqeql
    471. fneqeql2
    472. fnreseql
    473. chfnrn
    474. funfvop
    475. funfvbrb
    476. fvimacnvi
    477. fvimacnv
    478. funimass3
    479. funimass5
    480. funconstss
    481. fvimacnvALT
    482. elpreima
    483. elpreimad
    484. fniniseg
    485. fncnvima2
    486. fniniseg2
    487. unpreima
    488. inpreima
    489. difpreima
    490. respreima
    491. iinpreima
    492. intpreima
    493. fimacnv
    494. fimacnvinrn
    495. fimacnvinrn2
    496. fvn0ssdmfun
    497. fnopfv
    498. fvelrn
    499. nelrnfvne
    500. fveqdmss
    501. fveqressseq
    502. fnfvelrn
    503. ffvelrn
    504. ffvelrni
    505. ffvelrnda
    506. ffvelrnd
    507. rexrn
    508. ralrn
    509. elrnrexdm
    510. elrnrexdmb
    511. eldmrexrn
    512. eldmrexrnb
    513. fvcofneq
    514. ralrnmptw
    515. rexrnmptw
    516. ralrnmpt
    517. rexrnmpt
    518. f0cli
    519. dff2
    520. dff3
    521. dff4
    522. dffo3
    523. dffo4
    524. dffo5
    525. exfo
    526. foelrn
    527. foco2
    528. fmpt
    529. f1ompt
    530. fmpti
    531. fvmptelrn
    532. fmptd
    533. fmpttd
    534. fmpt3d
    535. fmptdf
    536. ffnfv
    537. ffnfvf
    538. fnfvrnss
    539. frnssb
    540. rnmptss
    541. fmpt2d
    542. ffvresb
    543. f1oresrab
    544. f1ossf1o
    545. fmptco
    546. fmptcof
    547. fmptcos
    548. cofmpt
    549. fcompt
    550. fcoconst
    551. fsn
    552. fsn2
    553. fsng
    554. fsn2g
    555. xpsng
    556. xpprsng
    557. xpsn
    558. f1o2sn
    559. residpr
    560. dfmpt
    561. fnasrn
    562. idref
    563. funiun
    564. funopsn
    565. funop
    566. funopdmsn
    567. funsndifnop
    568. funsneqopb
    569. ressnop0
    570. fpr
    571. fprg
    572. ftpg
    573. ftp
    574. fnressn
    575. funressn
    576. fressnfv
    577. fvrnressn
    578. fvressn
    579. fvn0fvelrn
    580. fvconst
    581. fnsnr
    582. fnsnb
    583. fmptsn
    584. fmptsng
    585. fmptsnd
    586. fmptap
    587. fmptapd
    588. fmptpr
    589. fvresi
    590. fninfp
    591. fnelfp
    592. fndifnfp
    593. fnelnfp
    594. fnnfpeq0
    595. fvunsn
    596. fvsng
    597. fvsn
    598. fvsnun1
    599. fvsnun2
    600. fnsnsplit
    601. fsnunf
    602. fsnunf2
    603. fsnunfv
    604. fsnunres
    605. funresdfunsn
    606. fvpr1
    607. fvpr2
    608. fvpr1g
    609. fvpr2g
    610. fprb
    611. fvtp1
    612. fvtp2
    613. fvtp3
    614. fvtp1g
    615. fvtp2g
    616. fvtp3g
    617. tpres
    618. fvconst2g
    619. fconst2g
    620. fvconst2
    621. fconst2
    622. fconst5
    623. rnmptc
    624. rnmptcOLD
    625. fnprb
    626. fntpb
    627. fnpr2g
    628. fpr2g
    629. fconstfv
    630. fconst3
    631. fconst4
    632. resfunexg
    633. resiexd
    634. fnex
    635. fnexd
    636. funex
    637. opabex
    638. mptexg
    639. mptexgf
    640. mptex
    641. mptexd
    642. mptrabex
    643. fex
    644. fexd
    645. mptfvmpt
    646. eufnfv
    647. funfvima
    648. funfvima2
    649. funfvima2d
    650. fnfvima
    651. fnfvimad
    652. resfvresima
    653. funfvima3
    654. rexima
    655. ralima
    656. fvclss
    657. elabrex
    658. abrexco
    659. imaiun
    660. imauni
    661. fniunfv
    662. funiunfv
    663. funiunfvf
    664. eluniima
    665. elunirn
    666. elunirnALT
    667. fnunirn
    668. dff13
    669. dff13f
    670. f1veqaeq
    671. f1cofveqaeq
    672. f1cofveqaeqALT
    673. 2f1fvneq
    674. f1mpt
    675. f1fveq
    676. f1elima
    677. f1imass
    678. f1imaeq
    679. f1imapss
    680. fpropnf1
    681. f1dom3fv3dif
    682. f1dom3el3dif
    683. dff14a
    684. dff14b
    685. f12dfv
    686. f13dfv
    687. dff1o6
    688. f1ocnvfv1
    689. f1ocnvfv2
    690. f1ocnvfv
    691. f1ocnvfvb
    692. nvof1o
    693. nvocnv
    694. fsnex
    695. f1prex
    696. f1ocnvdm
    697. f1ocnvfvrneq
    698. fcof1
    699. fcofo
    700. cbvfo
    701. cbvexfo
    702. cocan1
    703. cocan2
    704. fcof1oinvd
    705. fcof1od
    706. 2fcoidinvd
    707. fcof1o
    708. 2fvcoidd
    709. 2fvidf1od
    710. 2fvidinvd
    711. foeqcnvco
    712. f1eqcocnv
    713. f1eqcocnvOLD
    714. fveqf1o
    715. nf1const
    716. nf1oconst
    717. fliftrel
    718. fliftel
    719. fliftel1
    720. fliftcnv
    721. fliftfun
    722. fliftfund
    723. fliftfuns
    724. fliftf
    725. fliftval
    726. isoeq1
    727. isoeq2
    728. isoeq3
    729. isoeq4
    730. isoeq5
    731. nfiso
    732. isof1o
    733. isof1oidb
    734. isof1oopb
    735. isorel
    736. soisores
    737. soisoi
    738. isoid
    739. isocnv
    740. isocnv2
    741. isocnv3
    742. isores2
    743. isores1
    744. isores3
    745. isotr
    746. isomin
    747. isoini
    748. isoini2
    749. isofrlem
    750. isoselem
    751. isofr
    752. isose
    753. isofr2
    754. isopolem
    755. isopo
    756. isosolem
    757. isoso
    758. isowe
    759. isowe2
    760. f1oiso
    761. f1oiso2
    762. f1owe
    763. weniso
    764. weisoeq
    765. weisoeq2
    766. knatar
  16. Cantor's Theorem
    1. canth
    2. ncanth
  17. 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
  18. 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. fvmpopr2d
    157. ov3
    158. ov6g
    159. ovg
    160. ovres
    161. ovresd
    162. oprres
    163. oprssov
    164. fovrn
    165. fovrnda
    166. fovrnd
    167. fnrnov
    168. foov
    169. fnovrn
    170. ovelrn
    171. funimassov
    172. ovelimab
    173. ovima0
    174. ovconst2
    175. oprssdm
    176. nssdmovg
    177. ndmovg
    178. ndmov
    179. ndmovcl
    180. ndmovrcl
    181. ndmovcom
    182. ndmovass
    183. ndmovdistr
    184. ndmovord
    185. ndmovordi
    186. Variable-to-class conversion for operations
  19. 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
  20. 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
  21. 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