Metamath Proof Explorer
Table of Contents - 2.1.6. The universal class
- cvv
- vjust
- df-v
- dfv2
- vex
- vexOLD
- elv
- elvd
- el2v
- eqv
- eqvf
- abv
- abvALT
- isset
- issetf
- isseti
- issetri
- eqvisset
- elex
- elexi
- elexd
- elex2
- elex22
- prcnel
- ralv
- rexv
- reuv
- rmov
- rabab
- rexcom4b
- ceqsalt
- ceqsralt
- ceqsalg
- ceqsalgALT
- ceqsal
- ceqsalv
- ceqsalvOLD
- ceqsralv
- ceqsralvOLD
- gencl
- 2gencl
- 3gencl
- cgsexg
- cgsex2g
- cgsex4g
- cgsex4gOLD
- ceqsex
- ceqsexv
- ceqsexvOLD
- ceqsexv2d
- ceqsex2
- ceqsex2v
- ceqsex3v
- ceqsex4v
- ceqsex6v
- ceqsex8v
- gencbvex
- gencbvex2
- gencbval
- sbhypf
- vtoclgft
- vtocldf
- vtocld
- vtocldOLD
- vtocl2d
- vtoclf
- vtocl
- vtoclALT
- vtocl2
- vtocl3
- vtoclb
- vtoclgf
- vtoclg1f
- vtoclg
- vtoclgOLD
- vtoclbg
- vtocl2gf
- vtocl3gf
- vtocl2g
- vtocl3g
- vtoclgaf
- vtoclga
- vtocl2ga
- vtocl2gaf
- vtocl3gaf
- vtocl3ga
- vtocl3gaOLD
- vtocl4g
- vtocl4ga
- vtocleg
- vtoclegft
- vtoclef
- vtocle
- vtoclri
- spcimgft
- spcgft
- spcimgf
- spcimegf
- spcgf
- spcegf
- spcimdv
- spcdv
- spcimedv
- spcgv
- spcegv
- spcedv
- spc2egv
- spc2gv
- spc2ed
- spc2d
- spc3egv
- spc3gv
- spcv
- spcev
- spc2ev
- rspct
- rspcdf
- rspc
- rspce
- rspcimdv
- rspcimedv
- rspcdv
- rspcedv
- rspcebdv
- rspcv
- rspcvOLD
- rspccv
- rspcva
- rspccva
- rspcev
- rspcevOLD
- rspcdva
- rspcedvd
- rspcime
- rspceaimv
- rspcedeq1vd
- rspcedeq2vd
- rspc2
- rspc2gv
- rspc2v
- rspc2va
- rspc2ev
- rspc3v
- rspc3ev
- rspceeqv
- ralxpxfr2d
- rexraleqim
- eqvincg
- eqvinc
- eqvincf
- alexeqg
- ceqex
- ceqsexg
- ceqsexgv
- ceqsexgvOLD
- ceqsrexv
- ceqsrexbv
- ceqsrex2v
- clel2g
- clel2gOLD
- clel2
- clel3g
- clel3
- clel4g
- clel4
- clel4OLD
- clel5
- pm13.183
- rr19.3v
- rr19.28v
- elab6g
- elabd2
- elabd3
- elabgt
- elabgtOLD
- elabgf
- elabf
- elabg
- elabgOLD
- elab
- elabOLD
- elab2g
- elabd
- elab2
- elab4g
- elab3gf
- elab3g
- elab3
- elrabi
- elrabiOLD
- elrabf
- rabtru
- rabeqc
- elrab3t
- elrab
- elrab3
- elrabd
- elrab2
- ralab
- ralrab
- rexab
- rexrab
- ralab2
- ralab2OLD
- ralrab2
- rexab2
- rexab2OLD
- rexrab2
- abidnf
- dedhb
- nelrdva
- eqeu
- moeq
- eueq
- eueqi
- eueq2
- eueq3
- moeq3
- mosub
- mo2icl
- mob2
- moi2
- mob
- moi
- morex
- euxfr2w
- euxfrw
- euxfr2
- euxfr
- euind
- reu2
- reu6
- reu3
- reu6i
- eqreu
- rmo4
- reu4
- reu7
- reu8
- rmo3f
- rmo4f
- reu2eqd
- reueq
- rmoeq
- rmoan
- rmoim
- rmoimia
- rmoimi
- rmoimi2
- 2reu5a
- reuimrmo
- 2reuswap
- 2reuswap2
- reuxfrd
- reuxfr
- reuxfr1d
- reuxfr1ds
- reuxfr1
- reuind
- 2rmorex
- 2reu5lem1
- 2reu5lem2
- 2reu5lem3
- 2reu5
- 2reurmo
- 2reurex
- 2rmoswap
- 2rexreu