Metamath Proof Explorer
Table of Contents - 2.3. ZF Set Theory - add the Axiom of Power Sets
- Introduce the Axiom of Power Sets
- ax-pow
- zfpow
- axpow2
- axpow3
- elALT2
- dtruALT2
- dtrucor
- dtrucor2
- dvdemo1
- dvdemo2
- nfnid
- nfcvb
- vpwex
- pwexg
- pwexd
- pwex
- pwel
- abssexg
- snexALT
- p0ex
- p0exALT
- pp0ex
- ord3ex
- dtruALT
- axc16b
- eunex
- eusv1
- eusvnf
- eusvnfb
- eusv2i
- eusv2nf
- eusv2
- reusv1
- reusv2lem1
- reusv2lem2
- reusv2lem3
- reusv2lem4
- reusv2lem5
- reusv2
- reusv3i
- reusv3
- eusv4
- alxfr
- ralxfrd
- rexxfrd
- ralxfr2d
- rexxfr2d
- ralxfrd2
- rexxfrd2
- ralxfr
- ralxfrALT
- rexxfr
- rabxfrd
- rabxfr
- reuhypd
- reuhyp
- zfpair
- axprALT
- Derive the Axiom of Pairing
- axprlem1
- axprlem2
- axprlem3
- axprlem4
- axprlem5
- axpr
- ax-pr
- zfpair2
- snex
- prex
- sels
- el
- elALT
- dtru
- snelpwi
- snelpw
- prelpw
- prelpwi
- rext
- sspwb
- unipw
- univ
- pwtr
- ssextss
- ssext
- nssss
- pweqb
- intid
- moabex
- rmorabex
- euabex
- nnullss
- exss
- opex
- otex
- elopg
- elop
- opi1
- opi2
- opeluu
- op1stb
- brv
- Ordered pair theorem
- opnz
- opnzi
- opth1
- opth
- opthg
- opth1g
- opthg2
- opth2
- opthneg
- opthne
- otth2
- otth
- otthg
- eqvinop
- sbcop1
- sbcop
- copsexgw
- copsexg
- copsex2t
- copsex2g
- copsex2gOLD
- copsex4g
- 0nelop
- opwo0id
- opeqex
- oteqex2
- oteqex
- opcom
- moop2
- opeqsng
- opeqsn
- opeqpr
- snopeqop
- propeqop
- propssopi
- snopeqopsnid
- mosubopt
- mosubop
- euop2
- euotd
- opthwiener
- uniop
- uniopel
- opthhausdorff
- opthhausdorff0
- otsndisj
- otiunsndisj
- iunopeqop
- brsnop
- Ordered-pair class abstractions (cont.)
- opabidw
- opabid
- elopab
- rexopabb
- vopelopabsb
- opelopabsb
- brabsb
- opelopabt
- opelopabga
- brabga
- opelopab2a
- opelopaba
- braba
- opelopabg
- brabg
- opelopabgf
- opelopab2
- opelopab
- brab
- opelopabaf
- opelopabf
- ssopab2
- ssopab2bw
- eqopab2bw
- ssopab2b
- ssopab2i
- ssopab2dv
- eqopab2b
- opabn0
- opab0
- csbopab
- csbopabgALT
- csbmpt12
- csbmpt2
- iunopab
- elopabr
- elopabran
- rbropapd
- rbropap
- 2rbropap
- 0nelopab
- 0nelopabOLD
- brabv
- Power class of union and intersection
- pwin
- pwunssOLD
- pwssun
- pwundifOLD
- pwun
- The identity relation
- cid
- df-id
- dfid4
- dfid2
- dfid3
- dfid2OLD
- The membership relation (or epsilon relation)
- cep
- df-eprel
- epelg
- epeli
- epel
- 0sn0ep
- epn0
- Partial and total orderings
- wpo
- wor
- df-po
- df-so
- poss
- poeq1
- poeq2
- nfpo
- nfso
- pocl
- poclOLD
- ispod
- swopolem
- swopo
- poirr
- potr
- po2nr
- po3nr
- po2ne
- po0
- pofun
- sopo
- soss
- soeq1
- soeq2
- sonr
- sotr
- solin
- so2nr
- so3nr
- sotric
- sotrieq
- sotrieq2
- soasym
- sotr2
- issod
- issoi
- isso2i
- so0
- somo
- Founded and well-ordering relations
- wfr
- wse
- wwe
- df-fr
- df-se
- df-we
- dffr6
- frd
- fri
- friOLD
- seex
- exse
- dffr2
- dffr2ALT
- frc
- frss
- sess1
- sess2
- freq1
- freq2
- seeq1
- seeq2
- nffr
- nfse
- nfwe
- frirr
- fr2nr
- fr0
- frminex
- efrirr
- efrn2lp
- epse
- tz7.2
- dfepfr
- epfrc
- wess
- weeq1
- weeq2
- wefr
- weso
- wecmpep
- wetrep
- wefrc
- we0
- wereu
- wereu2
- Relations
- cxp
- ccnv
- cdm
- crn
- cres
- cima
- ccom
- wrel
- df-xp
- df-rel
- df-cnv
- df-co
- df-dm
- df-rn
- df-res
- df-ima
- xpeq1
- xpss12
- xpss
- inxpssres
- relxp
- xpss1
- xpss2
- xpeq2
- elxpi
- elxp
- elxp2
- xpeq12
- xpeq1i
- xpeq2i
- xpeq12i
- xpeq1d
- xpeq2d
- xpeq12d
- sqxpeqd
- nfxp
- 0nelxp
- 0nelelxp
- opelxp
- opelxpi
- opelxpd
- opelvv
- opelvvg
- opelxp1
- opelxp2
- otelxp1
- otel3xp
- opabssxpd
- rabxp
- brxp
- pwvrel
- pwvabrel
- brrelex12
- brrelex1
- brrelex2
- brrelex12i
- brrelex1i
- brrelex2i
- nprrel12
- nprrel
- 0nelrel0
- 0nelrel
- fconstmpt
- vtoclr
- opthprc
- brel
- elxp3
- opeliunxp
- xpundi
- xpundir
- xpiundi
- xpiundir
- iunxpconst
- xpun
- elvv
- elvvv
- elvvuni
- brinxp2
- brinxp
- opelinxp
- poinxp
- soinxp
- frinxp
- seinxp
- weinxp
- posn
- sosn
- frsn
- wesn
- elopaelxp
- bropaex12
- opabssxp
- brab2a
- optocl
- 2optocl
- 3optocl
- opbrop
- 0xp
- csbxp
- releq
- releqi
- releqd
- nfrel
- sbcrel
- relss
- ssrel
- eqrel
- ssrel2
- relssi
- relssdv
- eqrelriv
- eqrelriiv
- eqbrriv
- eqrelrdv
- eqbrrdv
- eqbrrdiv
- eqrelrdv2
- ssrelrel
- eqrelrel
- elrel
- rel0
- nrelv
- relsng
- relsnb
- relsnopg
- relsn
- relsnop
- copsex2gb
- copsex2ga
- elopaba
- xpsspw
- unixpss
- relun
- relin1
- relin2
- relinxp
- reldif
- reliun
- reliin
- reluni
- relint
- relopabiv
- relopabv
- relopabi
- relopabiALT
- relopab
- mptrel
- reli
- rele
- opabid2
- inopab
- difopab
- inxp
- xpindi
- xpindir
- xpiindi
- xpriindi
- eliunxp
- opeliunxp2
- raliunxp
- rexiunxp
- ralxp
- rexxp
- exopxfr
- exopxfr2
- djussxp
- ralxpf
- rexxpf
- iunxpf
- opabbi2dv
- relop
- ideqg
- ideq
- ididg
- issetid
- coss1
- coss2
- coeq1
- coeq2
- coeq1i
- coeq2i
- coeq1d
- coeq2d
- coeq12i
- coeq12d
- nfco
- brcog
- opelco2g
- brcogw
- eqbrrdva
- brco
- opelco
- cnvss
- cnveq
- cnveqi
- cnveqd
- elcnv
- elcnv2
- nfcnv
- brcnvg
- opelcnvg
- opelcnv
- brcnv
- csbcnv
- csbcnvgALT
- cnvco
- cnvuni
- dfdm3
- dfrn2
- dfrn3
- elrn2g
- elrng
- elrn2
- elrn
- ssrelrn
- dfdm4
- dfdmf
- csbdm
- eldmg
- eldm2g
- eldm
- eldm2
- dmss
- dmeq
- dmeqi
- dmeqd
- opeldmd
- opeldm
- breldm
- breldmg
- dmun
- dmin
- breldmd
- dmiun
- dmuni
- dmopab
- dmopabelb
- dmopab2rex
- dmopabss
- dmopab3
- dm0
- dmi
- dmv
- dmep
- domepOLD
- dm0rn0
- rn0
- rnep
- reldm0
- dmxp
- dmxpid
- dmxpin
- xpid11
- dmcnvcnv
- rncnvcnv
- elreldm
- rneq
- rneqi
- rneqd
- rnss
- rnssi
- brelrng
- brelrn
- opelrn
- releldm
- relelrn
- releldmb
- relelrnb
- releldmi
- relelrni
- dfrnf
- nfdm
- nfrn
- dmiin
- rnopab
- rnmpt
- elrnmpt
- elrnmpt1s
- elrnmpt1
- elrnmptg
- elrnmpti
- elrnmptd
- elrnmptdv
- elrnmpt2d
- dfiun3g
- dfiin3g
- dfiun3
- dfiin3
- riinint
- relrn0
- dmrnssfld
- dmcoss
- rncoss
- dmcosseq
- dmcoeq
- rncoeq
- reseq1
- reseq2
- reseq1i
- reseq2i
- reseq12i
- reseq1d
- reseq2d
- reseq12d
- nfres
- csbres
- res0
- dfres3
- opelres
- brres
- opelresi
- brresi
- opres
- resieq
- opelidres
- resres
- resundi
- resundir
- resindi
- resindir
- inres
- resdifcom
- resiun1
- resiun2
- dmres
- ssdmres
- dmresexg
- resss
- rescom
- ssres
- ssres2
- relres
- resabs1
- resabs1d
- resabs2
- residm
- resima
- resima2
- rnresss
- xpssres
- elinxp
- elres
- elsnres
- relssres
- dmressnsn
- eldmressnsn
- eldmeldmressn
- resdm
- resexg
- resexd
- resex
- resindm
- resdmdfsn
- resopab
- iss
- resopab2
- resmpt
- resmpt3
- resmptf
- resmptd
- dfres2
- mptss
- elidinxp
- elidinxpid
- elrid
- idinxpres
- idinxpresid
- idssxp
- opabresid
- mptresid
- opabresidOLD
- mptresidOLD
- dmresi
- restidsing
- iresn0n0
- imaeq1
- imaeq2
- imaeq1i
- imaeq2i
- imaeq1d
- imaeq2d
- imaeq12d
- dfima2
- dfima3
- elimag
- elima
- elima2
- elima3
- nfima
- nfimad
- imadmrn
- imassrn
- mptima
- imai
- rnresi
- resiima
- ima0
- 0ima
- csbima12
- imadisj
- cnvimass
- cnvimarndm
- imasng
- relimasn
- elrelimasn
- elimasng1
- elimasn1
- elimasng
- elimasn
- elimasngOLD
- elimasni
- args
- elinisegg
- eliniseg
- epin
- epini
- iniseg
- inisegn0
- dffr3
- dfse2
- imass1
- imass2
- ndmima
- relcnv
- relbrcnvg
- eliniseg2
- relbrcnv
- cotrg
- cotr
- idrefALT
- cnvsym
- intasym
- asymref
- asymref2
- intirr
- brcodir
- codir
- qfto
- xpidtr
- trin2
- poirr2
- trinxp
- soirri
- sotri
- son2lpi
- sotri2
- sotri3
- poleloe
- poltletr
- somin1
- somincom
- somin2
- soltmin
- cnvopab
- mptcnv
- cnv0
- cnvi
- cnvun
- cnvdif
- cnvin
- rnun
- rnin
- rniun
- rnuni
- imaundi
- imaundir
- cnvimassrndm
- dminss
- imainss
- inimass
- inimasn
- cnvxp
- xp0
- xpnz
- xpeq0
- xpdisj1
- xpdisj2
- xpsndisj
- difxp
- difxp1
- difxp2
- djudisj
- xpdifid
- resdisj
- rnxp
- dmxpss
- rnxpss
- rnxpid
- ssxpb
- xp11
- xpcan
- xpcan2
- ssrnres
- rninxp
- dminxp
- imainrect
- xpima
- xpima1
- xpima2
- xpimasn
- sossfld
- sofld
- cnvcnv3
- dfrel2
- dfrel4v
- dfrel4
- cnvcnv
- cnvcnv2
- cnvcnvss
- cnvrescnv
- cnveqb
- cnveq0
- dfrel3
- elid
- dmresv
- rnresv
- dfrn4
- csbrn
- rescnvcnv
- cnvcnvres
- imacnvcnv
- dmsnn0
- rnsnn0
- dmsn0
- cnvsn0
- dmsn0el
- relsn2
- dmsnopg
- dmsnopss
- dmpropg
- dmsnop
- dmprop
- dmtpop
- cnvcnvsn
- dmsnsnsn
- rnsnopg
- rnpropg
- cnvsng
- rnsnop
- op1sta
- cnvsn
- op2ndb
- op2nda
- opswap
- cnvresima
- resdm2
- resdmres
- resresdm
- imadmres
- resdmss
- resdifdi
- resdifdir
- mptpreima
- mptiniseg
- dmmpt
- dmmptss
- dmmptg
- rnmpt0f
- rnmptn0
- relco
- dfco2
- dfco2a
- coundi
- coundir
- cores
- resco
- imaco
- rnco
- rnco2
- dmco
- coeq0
- coiun
- cocnvcnv1
- cocnvcnv2
- cores2
- co02
- co01
- coi1
- coi2
- coires1
- coass
- relcnvtrg
- relcnvtr
- relssdmrn
- resssxp
- cnvssrndm
- cossxp
- relrelss
- unielrel
- relfld
- relresfld
- relcoi2
- relcoi1
- unidmrn
- relcnvfld
- dfdm2
- unixp
- unixp0
- unixpid
- ressn
- cnviin
- cnvpo
- cnvso
- xpco
- xpcoid
- elsnxp
- reu3op
- reuop
- opreu2reurex
- opreu2reu
- dfpo2
- csbcog
- The Predecessor Class
- cpred
- df-pred
- predeq123
- predeq1
- predeq2
- predeq3
- nfpred
- csbpredg
- predpredss
- predss
- sspred
- dfpred2
- dfpred3
- dfpred3g
- elpredgg
- elpredg
- elpredimg
- elpredim
- elpred
- predexg
- predasetexOLD
- dffr4
- predel
- predbrg
- predtrss
- predpo
- predso
- setlikespec
- predidm
- predin
- predun
- preddif
- predep
- trpred
- preddowncl
- predpoirr
- predfrirr
- pred0
- dfse3
- predrelss
- predprc
- predres
- Well-founded induction (variant)
- frpomin
- frpomin2
- frpoind
- frpoinsg
- frpoins2fg
- frpoins2g
- frpoins3g
- Well-ordered induction
- tz6.26
- tz6.26OLD
- tz6.26i
- wfi
- wfiOLD
- wfii
- wfisg
- wfisgOLD
- wfis
- wfis2fg
- wfis2fgOLD
- wfis2f
- wfis2g
- wfis2
- wfis3
- Ordinals
- word
- con0
- wlim
- csuc
- df-ord
- df-on
- df-lim
- df-suc
- ordeq
- elong
- elon
- eloni
- elon2
- limeq
- ordwe
- ordtr
- ordfr
- ordelss
- trssord
- ordirr
- nordeq
- ordn2lp
- tz7.5
- ordelord
- tron
- ordelon
- onelon
- tz7.7
- ordelssne
- ordelpss
- ordsseleq
- ordin
- onin
- ordtri3or
- ordtri1
- ontri1
- ordtri2
- ordtri3
- ordtri4
- orddisj
- onfr
- onelpss
- onsseleq
- onelss
- ordtr1
- ordtr2
- ordtr3
- ontr1
- ontr2
- ordunidif
- ordintdif
- onintss
- oneqmini
- ord0
- 0elon
- ord0eln0
- on0eln0
- dflim2
- inton
- nlim0
- limord
- limuni
- limuni2
- 0ellim
- limelon
- onn0
- suceq
- elsuci
- elsucg
- elsuc2g
- elsuc
- elsuc2
- nfsuc
- elelsuc
- sucel
- suc0
- sucprc
- unisuc
- sssucid
- sucidg
- sucid
- nsuceq0
- eqelsuc
- iunsuc
- suctr
- trsuc
- trsucss
- ordsssuc
- onsssuc
- ordsssuc2
- onmindif
- ordnbtwn
- onnbtwn
- sucssel
- orddif
- orduniss
- ordtri2or
- ordtri2or2
- ordtri2or3
- ordelinel
- ordssun
- ordequn
- ordun
- ordunisssuc
- suc11
- onun2
- onordi
- ontrci
- onirri
- oneli
- onelssi
- onssneli
- onssnel2i
- onelini
- oneluni
- onunisuci
- onsseli
- onun2i
- unizlim
- on0eqel
- snsn0non
- onxpdisj
- onnev
- onnevOLD
- Definite description binder (inverted iota)
- cio
- iotajust
- df-iota
- dfiota2
- nfiota1
- nfiotadw
- nfiotaw
- nfiotad
- nfiota
- cbviotaw
- cbviotavw
- cbviotavwOLD
- cbviota
- cbviotav
- sb8iota
- iotaeq
- iotabi
- uniabio
- iotaval
- iotauni
- iotaint
- iota1
- iotanul
- iotassuni
- iotaex
- iota4
- iota4an
- iota5
- iotabidv
- iotabii
- iotacl
- iota2df
- iota2d
- iota2
- iotan0
- sniota
- dfiota4
- csbiota
- Functions
- wfun
- wfn
- wf
- wf1
- wfo
- wf1o
- cfv
- wiso
- df-fun
- df-fn
- df-f
- df-f1
- df-fo
- df-f1o
- df-fv
- df-isom
- dffun2
- dffun3
- dffun4
- dffun5
- dffun6f
- dffun6
- funmo
- funrel
- 0nelfun
- funss
- funeq
- funeqi
- funeqd
- nffun
- sbcfung
- funeu
- funeu2
- dffun7
- dffun8
- dffun9
- funfn
- funfnd
- funi
- nfunv
- funopg
- funopab
- funopabeq
- funopab4
- funmpt
- funmpt2
- funco
- funresfunco
- funres
- funresd
- funssres
- fun2ssres
- funun
- fununmo
- fununfun
- fundif
- funcnvsn
- funsng
- fnsng
- funsn
- funprg
- funtpg
- funpr
- funtp
- fnsn
- fnprg
- fntpg
- fntp
- funcnvpr
- funcnvtp
- funcnvqp
- fun0
- funcnv0
- funcnvcnv
- funcnv2
- funcnv
- funcnv3
- fun2cnv
- svrelfun
- fncnv
- fun11
- fununi
- funin
- funres11
- funcnvres
- cnvresid
- funcnvres2
- funimacnv
- funimass1
- funimass2
- imadif
- imain
- funimaexg
- funimaex
- isarep1
- isarep2
- fneq1
- fneq2
- fneq1d
- fneq2d
- fneq12d
- fneq12
- fneq1i
- fneq2i
- nffn
- fnfun
- fnfund
- fnrel
- fndm
- fndmi
- fndmd
- funfni
- fndmu
- fnbr
- fnop
- fneu
- fneu2
- fnun
- fnund
- fnunop
- fncofn
- fnco
- fncoOLD
- fnresdm
- fnresdisj
- 2elresin
- fnssresb
- fnssres
- fnssresd
- fnresin1
- fnresin2
- fnres
- idfn
- fnresi
- fnresiOLD
- fnima
- fn0
- fnimadisj
- fnimaeq0
- dfmpt3
- mptfnf
- fnmptf
- fnopabg
- fnopab
- mptfng
- fnmpt
- fnmptd
- mpt0
- fnmpti
- dmmpti
- dmmptd
- mptun
- partfun
- feq1
- feq2
- feq3
- feq23
- feq1d
- feq2d
- feq3d
- feq12d
- feq123d
- feq123
- feq1i
- feq2i
- feq12i
- feq23i
- feq23d
- nff
- sbcfng
- sbcfg
- elimf
- ffn
- ffnd
- dffn2
- ffun
- ffund
- frel
- freld
- frn
- frnd
- fdm
- fdmOLD
- fdmd
- fdmi
- dffn3
- ffrn
- ffrnb
- ffrnbd
- fss
- fssd
- fssdmd
- fssdm
- fimass
- fimacnv
- fcof
- fco
- fcoOLD
- fcod
- fco2
- fssxp
- funssxp
- ffdm
- ffdmd
- fdmrn
- funcofd
- fco3OLD
- opelf
- fun
- fun2
- fun2d
- fnfco
- fssres
- fssresd
- fssres2
- fresin
- resasplit
- fresaun
- fresaunres2
- fresaunres1
- fcoi1
- fcoi2
- feu
- fcnvres
- fimacnvdisj
- fint
- fin
- f0
- f00
- f0bi
- f0dom0
- f0rn0
- fconst
- fconstg
- fnconstg
- fconst6g
- fconst6
- f1eq1
- f1eq2
- f1eq3
- nff1
- dff12
- f1f
- f1fn
- f1fun
- f1rel
- f1dm
- f1dmOLD
- f1ss
- f1ssr
- f1ssres
- f1resf1
- f1cnvcnv
- f1cof1
- f1co
- f1coOLD
- foeq1
- foeq2
- foeq3
- nffo
- fof
- fofun
- fofn
- forn
- dffo2
- foima
- dffn4
- funforn
- fodmrnu
- fimadmfo
- fores
- fimadmfoALT
- focnvimacdmdm
- focofo
- foco
- foconst
- f1oeq1
- f1oeq2
- f1oeq3
- f1oeq23
- f1eq123d
- foeq123d
- f1oeq123d
- f1oeq1d
- f1oeq2d
- f1oeq3d
- nff1o
- f1of1
- f1of
- f1ofn
- f1ofun
- f1orel
- f1odm
- dff1o2
- dff1o3
- f1ofo
- dff1o4
- dff1o5
- f1orn
- f1f1orn
- f1ocnv
- f1ocnvb
- f1ores
- f1orescnv
- f1imacnv
- foimacnv
- foun
- f1oun
- resdif
- resin
- f1oco
- f1cnv
- funcocnv2
- fococnv2
- f1ococnv2
- f1cocnv2
- f1ococnv1
- f1cocnv1
- funcoeqres
- f1ssf1
- f10
- f10d
- f1o00
- fo00
- f1o0
- f1oi
- f1ovi
- f1osn
- f1osng
- f1sng
- fsnd
- f1oprswap
- f1oprg
- tz6.12-2
- fveu
- brprcneu
- brprcneuALT
- fvprc
- fvprcALT
- rnfvprc
- fv2
- dffv3
- dffv4
- elfv
- fveq1
- fveq2
- fveq1i
- fveq1d
- fveq2i
- fveq2d
- 2fveq3
- fveq12i
- fveq12d
- fveqeq2d
- fveqeq2
- nffv
- nffvmpt1
- nffvd
- fvex
- fvexi
- fvexd
- fvif
- iffv
- fv3
- fvres
- fvresd
- funssfv
- tz6.12-1
- tz6.12
- tz6.12f
- tz6.12c
- tz6.12i
- fvbr0
- fvrn0
- fvssunirn
- ndmfv
- ndmfvrcl
- elfvdm
- elfvex
- elfvexd
- eliman0
- nfvres
- nfunsn
- fvfundmfvn0
- 0fv
- fv2prc
- elfv2ex
- fveqres
- csbfv12
- csbfv2g
- csbfv
- funbrfv
- funopfv
- fnbrfvb
- fnopfvb
- funbrfvb
- funopfvb
- fnbrfvb2
- funbrfv2b
- dffn5
- fnrnfv
- fvelrnb
- foelrni
- dfimafn
- dfimafn2
- funimass4
- fvelima
- fvelimad
- feqmptd
- feqresmpt
- feqmptdf
- dffn5f
- fvelimab
- fvelimabd
- unima
- fvi
- fviss
- fniinfv
- fnsnfv
- fnsnfvOLD
- opabiotafun
- opabiotadm
- opabiota
- fnimapr
- ssimaex
- ssimaexg
- funfv
- funfv2
- funfv2f
- fvun
- fvun1
- fvun2
- fvun1d
- fvun2d
- dffv2
- dmfco
- fvco2
- fvco
- fvco3
- fvco3d
- fvco4i
- fvopab3g
- fvopab3ig
- brfvopabrbr
- fvmptg
- fvmpti
- fvmpt
- fvmpt2f
- fvtresfn
- fvmpts
- fvmpt3
- fvmpt3i
- fvmptdf
- fvmptd
- fvmptd2
- mptrcl
- fvmpt2i
- fvmpt2
- fvmptss
- fvmpt2d
- fvmptex
- fvmptd3f
- fvmptd2f
- fvmptdv
- fvmptdv2
- mpteqb
- fvmptt
- fvmptf
- fvmptnf
- fvmptd3
- fvmptn
- fvmptss2
- elfvmptrab1w
- elfvmptrab1
- elfvmptrab
- fvopab4ndm
- fvmptndm
- fvmptrabfv
- fvopab5
- fvopab6
- eqfnfv
- eqfnfv2
- eqfnfv3
- eqfnfvd
- eqfnfv2f
- eqfunfv
- fvreseq0
- fvreseq1
- fvreseq
- fnmptfvd
- fndmdif
- fndmdifcom
- fndmdifeq0
- fndmin
- fneqeql
- fneqeql2
- fnreseql
- chfnrn
- funfvop
- funfvbrb
- fvimacnvi
- fvimacnv
- funimass3
- funimass5
- funconstss
- fvimacnvALT
- elpreima
- elpreimad
- fniniseg
- fncnvima2
- fniniseg2
- unpreima
- inpreima
- difpreima
- respreima
- cnvimainrn
- sspreima
- iinpreima
- intpreima
- fimacnvOLD
- fimacnvinrn
- fimacnvinrn2
- rescnvimafod
- fvn0ssdmfun
- fnopfv
- fvelrn
- nelrnfvne
- fveqdmss
- fveqressseq
- fnfvelrn
- ffvelrn
- ffvelrni
- ffvelrnda
- ffvelrnd
- rexrn
- ralrn
- elrnrexdm
- elrnrexdmb
- eldmrexrn
- eldmrexrnb
- fvcofneq
- ralrnmptw
- rexrnmptw
- ralrnmpt
- rexrnmpt
- f0cli
- dff2
- dff3
- dff4
- dffo3
- dffo4
- dffo5
- exfo
- foelrn
- foco2
- fmpt
- f1ompt
- fmpti
- fvmptelrn
- fmptd
- fmpttd
- fmpt3d
- fmptdf
- ffnfv
- ffnfvf
- fnfvrnss
- frnssb
- rnmptss
- fmpt2d
- ffvresb
- f1oresrab
- f1ossf1o
- fmptco
- fmptcof
- fmptcos
- cofmpt
- fcompt
- fcoconst
- fsn
- fsn2
- fsng
- fsn2g
- xpsng
- xpprsng
- xpsn
- f1o2sn
- residpr
- dfmpt
- fnasrn
- idref
- funiun
- funopsn
- funop
- funopdmsn
- funsndifnop
- funsneqopb
- ressnop0
- fpr
- fprg
- ftpg
- ftp
- fnressn
- funressn
- fressnfv
- fvrnressn
- fvressn
- fvn0fvelrn
- fvconst
- fnsnr
- fnsnb
- fmptsn
- fmptsng
- fmptsnd
- fmptap
- fmptapd
- fmptpr
- fvresi
- fninfp
- fnelfp
- fndifnfp
- fnelnfp
- fnnfpeq0
- fvunsn
- fvsng
- fvsn
- fvsnun1
- fvsnun2
- fnsnsplit
- fsnunf
- fsnunf2
- fsnunfv
- fsnunres
- funresdfunsn
- fvpr1g
- fvpr2g
- fvpr2gOLD
- fvpr1
- fvpr1OLD
- fvpr2
- fvpr2OLD
- fprb
- fvtp1
- fvtp2
- fvtp3
- fvtp1g
- fvtp2g
- fvtp3g
- tpres
- fvconst2g
- fconst2g
- fvconst2
- fconst2
- fconst5
- rnmptc
- rnmptcOLD
- fnprb
- fntpb
- fnpr2g
- fpr2g
- fconstfv
- fconst3
- fconst4
- resfunexg
- resiexd
- fnex
- fnexd
- funex
- opabex
- mptexg
- mptexgf
- mptex
- mptexd
- mptrabex
- fex
- fexd
- mptfvmpt
- eufnfv
- funfvima
- funfvima2
- funfvima2d
- fnfvima
- fnfvimad
- resfvresima
- funfvima3
- rexima
- ralima
- fvclss
- elabrex
- abrexco
- imaiun
- imauni
- fniunfv
- funiunfv
- funiunfvf
- eluniima
- elunirn
- elunirnALT
- elunirn2
- fnunirn
- dff13
- dff13f
- f1veqaeq
- f1cofveqaeq
- f1cofveqaeqALT
- 2f1fvneq
- f1mpt
- f1fveq
- f1elima
- f1imass
- f1imaeq
- f1imapss
- fpropnf1
- f1dom3fv3dif
- f1dom3el3dif
- dff14a
- dff14b
- f12dfv
- f13dfv
- dff1o6
- f1ocnvfv1
- f1ocnvfv2
- f1ocnvfv
- f1ocnvfvb
- nvof1o
- nvocnv
- fsnex
- f1prex
- f1ocnvdm
- f1ocnvfvrneq
- fcof1
- fcofo
- cbvfo
- cbvexfo
- cocan1
- cocan2
- fcof1oinvd
- fcof1od
- 2fcoidinvd
- fcof1o
- 2fvcoidd
- 2fvidf1od
- 2fvidinvd
- foeqcnvco
- f1eqcocnv
- f1eqcocnvOLD
- fveqf1o
- nf1const
- nf1oconst
- f1ofvswap
- fliftrel
- fliftel
- fliftel1
- fliftcnv
- fliftfun
- fliftfund
- fliftfuns
- fliftf
- fliftval
- isoeq1
- isoeq2
- isoeq3
- isoeq4
- isoeq5
- nfiso
- isof1o
- isof1oidb
- isof1oopb
- isorel
- soisores
- soisoi
- isoid
- isocnv
- isocnv2
- isocnv3
- isores2
- isores1
- isores3
- isotr
- isomin
- isoini
- isoini2
- isofrlem
- isoselem
- isofr
- isose
- isofr2
- isopolem
- isopo
- isosolem
- isoso
- isowe
- isowe2
- f1oiso
- f1oiso2
- f1owe
- weniso
- weisoeq
- weisoeq2
- knatar
- Cantor's Theorem
- canth
- ncanth
- Restricted iota (description binder)
- crio
- df-riota
- riotaeqdv
- riotabidv
- riotaeqbidv
- riotaex
- riotav
- riotauni
- nfriota1
- nfriotadw
- cbvriotaw
- cbvriotavw
- cbvriotavwOLD
- nfriotad
- nfriota
- cbvriota
- cbvriotav
- csbriota
- riotacl2
- riotacl
- riotasbc
- riotabidva
- riotabiia
- riota1
- riota1a
- riota2df
- riota2f
- riota2
- riotaeqimp
- riotaprop
- riota5f
- riota5
- riotass2
- riotass
- moriotass
- snriota
- riotaxfrd
- eusvobj2
- eusvobj1
- f1ofveu
- f1ocnvfv3
- riotaund
- riotassuni
- riotaclb
- Operations
- co
- coprab
- cmpo
- df-ov
- df-oprab
- df-mpo
- oveq
- oveq1
- oveq2
- oveq12
- oveq1i
- oveq2i
- oveq12i
- oveqi
- oveq123i
- oveq1d
- oveq2d
- oveqd
- oveq12d
- oveqan12d
- oveqan12rd
- oveq123d
- fvoveq1d
- fvoveq1
- ovanraleqv
- imbrov2fvoveq
- ovrspc2v
- oveqrspc2v
- oveqdr
- nfovd
- nfov
- oprabidw
- oprabid
- ovex
- ovexi
- ovexd
- ovssunirn
- 0ov
- ovprc
- ovprc1
- ovprc2
- ovrcl
- csbov123
- csbov
- csbov12g
- csbov1g
- csbov2g
- rspceov
- elovimad
- fnbrovb
- fnotovb
- opabbrex
- opabresex2d
- fvmptopab
- f1opr
- brfvopab
- dfoprab2
- reloprab
- oprabv
- nfoprab1
- nfoprab2
- nfoprab3
- nfoprab
- oprabbid
- oprabbidv
- oprabbii
- ssoprab2
- ssoprab2b
- eqoprab2bw
- eqoprab2b
- mpoeq123
- mpoeq12
- mpoeq123dva
- mpoeq123dv
- mpoeq123i
- mpoeq3dva
- mpoeq3ia
- mpoeq3dv
- nfmpo1
- nfmpo2
- nfmpo
- 0mpo0
- mpo0v
- mpo0
- oprab4
- cbvoprab1
- cbvoprab2
- cbvoprab12
- cbvoprab12v
- cbvoprab3
- cbvoprab3v
- cbvmpox
- cbvmpo
- cbvmpov
- elimdelov
- ovif
- ovif2
- ovif12
- ifov
- dmoprab
- dmoprabss
- rnoprab
- rnoprab2
- reldmoprab
- oprabss
- eloprabga
- eloprabgaOLD
- eloprabg
- ssoprab2i
- mpov
- mpomptx
- mpompt
- mpodifsnif
- mposnif
- fconstmpo
- resoprab
- resoprab2
- resmpo
- funoprabg
- funoprab
- fnoprabg
- mpofun
- mpofunOLD
- fnoprab
- ffnov
- fovcl
- eqfnov
- eqfnov2
- fnov
- mpo2eqb
- rnmpo
- reldmmpo
- elrnmpog
- elrnmpo
- elrnmpores
- ralrnmpo
- rexrnmpo
- ovid
- ovidig
- ovidi
- ov
- ovigg
- ovig
- ovmpt4g
- ovmpos
- ov2gf
- ovmpodxf
- ovmpodx
- ovmpod
- ovmpox
- ovmpoga
- ovmpoa
- ovmpodf
- ovmpodv
- ovmpodv2
- ovmpog
- ovmpo
- fvmpopr2d
- ov3
- ov6g
- ovg
- ovres
- ovresd
- oprres
- oprssov
- fovrn
- fovrnda
- fovrnd
- fnrnov
- foov
- fnovrn
- ovelrn
- funimassov
- ovelimab
- ovima0
- ovconst2
- oprssdm
- nssdmovg
- ndmovg
- ndmov
- ndmovcl
- ndmovrcl
- ndmovcom
- ndmovass
- ndmovdistr
- ndmovord
- ndmovordi
- Variable-to-class conversion for operations
- Maps-to notation
- mpondm0
- elmpocl
- elmpocl1
- elmpocl2
- elovmpo
- elovmporab
- elovmporab1w
- elovmporab1
- 2mpo0
- relmptopab
- f1ocnvd
- f1od
- f1ocnv2d
- f1o2d
- f1opw2
- f1opw
- elovmpt3imp
- ovmpt3rab1
- ovmpt3rabdm
- elovmpt3rab1
- elovmpt3rab
- Function operation
- cof
- cofr
- df-of
- df-ofr
- ofeqd
- ofeq
- ofreq
- ofexg
- nfof
- nfofr
- ofrfvalg
- offval
- ofrfval
- ofval
- ofrval
- offn
- offun
- offval2f
- ofmresval
- fnfvof
- off
- ofres
- offval2
- ofrfval2
- ofmpteq
- ofco
- offveq
- offveqb
- ofc1
- ofc2
- ofc12
- caofref
- caofinvl
- caofid0l
- caofid0r
- caofid1
- caofid2
- caofcom
- caofrss
- caofass
- caoftrn
- caofdi
- caofdir
- caonncan
- Proper subset relation
- crpss
- df-rpss
- relrpss
- brrpssg
- brrpss
- porpss
- sorpss
- sorpssi
- sorpssun
- sorpssin
- sorpssuni
- sorpssint
- sorpsscmpl