Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Metamath Proof Explorer
Table of Contents - 20.16.4. First-order logic
Utility lemmas or strengthenings of theorems in the main part (biconditional
or closed forms, or fewer disjoint variable conditions, or disjoint variable
conditions replaced with nonfreeness hypotheses...). Sorted in the same
order as in the main part.
Universal and existential quantifiers, nonfreeness predicate
Adding ax-gen
bj-genr
bj-genl
bj-genan
bj-mpgs
Adding ax-4
bj-2alim
bj-2exim
bj-alanim
bj-2albi
bj-notalbii
bj-2exbi
bj-3exbi
bj-sylgt2
bj-alrimg
bj-alrimd
bj-sylget
bj-sylget2
bj-exlimg
bj-sylge
bj-exlimd
bj-nfimexal
bj-alexim
bj-nexdh
bj-nexdh2
bj-hbxfrbi
bj-hbyfrbi
bj-exalim
bj-exalimi
bj-exalims
bj-exalimsi
bj-ax12ig
bj-ax12i
bj-nfimt
bj-cbvalimt
bj-cbveximt
bj-eximALT
bj-aleximiALT
bj-eximcom
Adding ax-5
bj-ax12wlem
bj-cbvalim
bj-cbvexim
bj-cbvalimi
bj-cbveximi
bj-cbval
bj-cbvex
wmoo
df-bj-mo
Equality and substitution
bj-ssbeq
bj-ssblem1
bj-ssblem2
bj-ax12v
bj-ax12
bj-ax12ssb
bj-19.41al
bj-equsexval
bj-subst
bj-ssbid2
bj-ssbid2ALT
bj-ssbid1
bj-ssbid1ALT
bj-ax6elem1
bj-ax6elem2
bj-ax6e
Adding ax-6
bj-spimvwt
bj-spnfw
bj-cbvexiw
bj-cbvexivw
bj-modald
bj-denot
bj-eqs
Adding ax-7
bj-cbvexw
bj-ax12w
Membership predicate, ax-8 and ax-9
bj-ax89
bj-elequ12
bj-cleljusti
Logical redundancy of ax-10--13
Adding ax-10
Adding ax-11
bj-alcomexcom
bj-hbalt
Adding ax-12
axc11n11
axc11n11r
bj-axc16g16
bj-ax12v3
bj-ax12v3ALT
bj-sb
bj-modalbe
bj-spst
bj-19.21bit
bj-19.23bit
bj-nexrt
bj-alrim
bj-alrim2
bj-nfdt0
bj-nfdt
bj-nexdt
bj-nexdvt
bj-alexbiex
bj-exexbiex
bj-alalbial
bj-exalbial
bj-19.9htbi
bj-hbntbi
bj-biexal1
bj-biexal2
bj-biexal3
bj-bialal
bj-biexex
bj-hbext
bj-nfalt
bj-nfext
bj-eeanvw
bj-modal4
bj-modal4e
bj-modalb
bj-wnf1
bj-wnf2
bj-wnfanf
bj-wnfenf
bj-substax12
bj-substw
Really adding ax-12
Nonfreeness
wnnf
df-bj-nnf
bj-nnfbi
bj-nnfbd
bj-nnfbii
bj-nnfa
bj-nnfad
bj-nnfai
bj-nnfe
bj-nnfed
bj-nnfei
bj-nnfea
bj-nnfead
bj-nnfeai
bj-dfnnf2
bj-nnfnfTEMP
bj-wnfnf
bj-nnfnt
bj-nnftht
bj-nnfth
bj-nnfnth
bj-nnfim1
bj-nnfim2
bj-nnfim
bj-nnfimd
bj-nnfan
bj-nnfand
bj-nnfor
bj-nnford
bj-nnfbit
bj-nnfbid
bj-nnfv
bj-nnf-alrim
bj-nnf-exlim
bj-dfnnf3
bj-nfnnfTEMP
bj-nnfa1
bj-nnfe1
bj-19.12
bj-nnflemaa
bj-nnflemee
bj-nnflemae
bj-nnflemea
bj-nnfalt
bj-nnfext
bj-stdpc5t
bj-19.21t
bj-19.23t
bj-19.36im
bj-19.37im
bj-19.42t
bj-19.41t
bj-sbft
bj-pm11.53vw
bj-pm11.53v
bj-pm11.53a
bj-equsvt
bj-equsalvwd
bj-equsexvwd
bj-sbievwd
Adding ax-13
bj-axc10
bj-alequex
bj-spimt2
bj-cbv3ta
bj-cbv3tb
bj-hbsb3t
bj-hbsb3
bj-nfs1t
bj-nfs1t2
bj-nfs1
Removing dependencies on ax-13 (and ax-11)
bj-axc10v
bj-spimtv
bj-cbv3hv2
bj-cbv1hv
bj-cbv2hv
bj-cbv2v
bj-cbvaldv
bj-cbvexdv
bj-cbval2vv
bj-cbvex2vv
bj-cbvaldvav
bj-cbvexdvav
bj-cbvex4vv
bj-equsalhv
bj-axc11nv
bj-aecomsv
bj-axc11v
bj-drnf2v
bj-equs45fv
bj-hbs1
bj-nfs1v
bj-hbsb2av
bj-hbsb3v
bj-nfsab1
bj-dtru
bj-dtrucor2v
Strengthenings of theorems of the main part
Distinct var metavariables
bj-hbaeb2
bj-hbaeb
bj-hbnaeb
bj-dvv
Around ~ equsal
bj-equsal1t
bj-equsal1ti
bj-equsal1
bj-equsal2
bj-equsal
Some Principia Mathematica proofs
stdpc5t
bj-stdpc5
2stdpc5
bj-19.21t0
exlimii
ax11-pm
ax6er
exlimiieq1
exlimiieq2
ax11-pm2
Alternate definition of substitution
bj-sbsb
bj-dfsb2
Lemmas for substitution
bj-sbf3
bj-sbf4
bj-sbnf
Existential uniqueness
bj-eu3f
First-order logic: miscellaneous
bj-sblem1
bj-sblem2
bj-sblem
bj-sbievw1
bj-sbievw2
bj-sbievw
bj-sbievv
bj-moeub
bj-sbidmOLD
bj-dvelimdv
bj-dvelimdv1
bj-dvelimv
bj-nfeel2
bj-axc14nf
bj-axc14
mobidvALT
sbn1ALT