Metamath Proof Explorer
Table of Contents - 20.33.1. Short Studies
- Additional work on conditional logical operator
- ifpan123g
- ifpan23
- ifpdfor2
- ifporcor
- ifpdfan2
- ifpancor
- ifpdfor
- ifpdfan
- ifpbi2
- ifpbi3
- ifpim1
- ifpnot
- ifpid2
- ifpim2
- ifpbi23
- ifpbiidcor
- ifpbicor
- ifpxorcor
- ifpbi1
- ifpnot23
- ifpnotnotb
- ifpnorcor
- ifpnancor
- ifpnot23b
- ifpbiidcor2
- ifpnot23c
- ifpnot23d
- ifpdfnan
- ifpdfxor
- ifpbi12
- ifpbi13
- ifpbi123
- ifpidg
- ifpid3g
- ifpid2g
- ifpid1g
- ifpim23g
- ifpim3
- ifpnim1
- ifpim4
- ifpnim2
- ifpim123g
- ifpim1g
- ifp1bi
- ifpbi1b
- ifpimimb
- ifpororb
- ifpananb
- ifpnannanb
- ifpor123g
- ifpimim
- ifpbibib
- ifpxorxorb
- Sophisms
- rp-fakeimass
- rp-fakeanorass
- rp-fakeoranass
- rp-fakeinunass
- rp-fakeuninass
- Finite Sets
- rp-isfinite5
- rp-isfinite6
- General Observations
- intabssd
- eu0
- epelon2
- ontric3g
- dfsucon
- snen1g
- snen1el
- sn1dom
- pr2dom
- tr3dom
- ensucne0
- ensucne0OLD
- dfom6
- infordmin
- iscard4
- iscard5
- elrncard
- harval3
- harval3on
- en2pr
- pr2cv
- pr2el1
- pr2cv1
- pr2el2
- pr2cv2
- pren2
- pr2eldif1
- pr2eldif2
- pren2d
- aleph1min
- alephiso2
- alephiso3
- Infinite Sets
- pwelg
- pwinfig
- pwinfi2
- pwinfi3
- pwinfi
- Finite intersection property
- fipjust
- cllem0
- superficl
- superuncl
- ssficl
- ssuncl
- ssdifcl
- sssymdifcl
- fiinfi
- RP ADDTO: Subclasses and subsets
- rababg
- RP ADDTO: The intersection of a class
- elintabg
- elinintab
- elmapintrab
- RP ADDTO: Theorems requiring subset and intersection existence
- elinintrab
- inintabss
- inintabd
- RP ADDTO: Relations
- xpinintabd
- relintabex
- elcnvcnvintab
- relintab
- nonrel
- elnonrel
- cnvssb
- relnonrel
- cnvnonrel
- brnonrel
- dmnonrel
- rnnonrel
- resnonrel
- imanonrel
- cononrel1
- cononrel2
- RP ADDTO: Functions
- elmapintab
- fvnonrel
- elinlem
- elcnvcnvlem
- RP ADDTO: Finite induction (for finite ordinals)
- cnvcnvintabd
- RP ADDTO: First and second members of an ordered pair
- elcnvlem
- elcnvintab
- cnvintabd
- RP ADDTO: The reflexive and transitive properties of relations
- undmrnresiss
- reflexg
- cnvssco
- refimssco
- RP ADDTO: Basic properties of closures
- cleq2lem
- cbvcllem
- clublem
- clss2lem
- dfid7
- mptrcllem
- cotrintab
- rclexi
- rtrclexlem
- rtrclex
- trclubgNEW
- trclubNEW
- trclexi
- rtrclexi
- clrellem
- clcnvlem
- cnvtrucl0
- cnvrcl0
- cnvtrcl0
- dmtrcl
- rntrcl
- dfrtrcl5
- RP REPLACE: Definitions and basic properties of transitive closures
- trcleq2lemRP
- Additions for square root; absolute value
- sqrtcvallem1
- reabsifneg
- reabsifnpos
- reabsifpos
- reabsifnneg
- reabssgn
- sqrtcvallem2
- sqrtcvallem3
- sqrtcvallem4
- sqrtcvallem5
- sqrtcval
- sqrtcval2
- resqrtval
- imsqrtval
- resqrtvalex
- imsqrtvalex