Type  Label  Description 
Statement 

Theorem  sb4b 1601 
Simplified definition of substitution when variables are distinct.
(Contributed by NM, 27May1997.)



Theorem  sb4bor 1602 
Simplified definition of substitution when variables are distinct,
expressed via disjunction. (Contributed by Jim Kingdon, 18Mar2018.)



Theorem  hbsb2 1603 
Boundvariable hypothesis builder for substitution. (Contributed by NM,
5Aug1993.)



Theorem  nfsb2or 1604 
Boundvariable hypothesis builder for substitution. Similar to hbsb2 1603
but in intuitionistic logic a disjunction is stronger than an
implication. (Contributed by Jim Kingdon, 2Feb2018.)



Theorem  sbequilem 1605 
Propositional logic lemma used in the sbequi 1606 proof. (Contributed by
Jim Kingdon, 1Feb2018.)



Theorem  sbequi 1606 
An equality theorem for substitution. (Contributed by NM, 5Aug1993.)
(Proof modified by Jim Kingdon, 1Feb2018.)



Theorem  sbequ 1607 
An equality theorem for substitution. Used in proof of Theorem 9.7 in
[Megill] p. 449 (p. 16 of the preprint).
(Contributed by NM,
5Aug1993.)



Theorem  drsb2 1608 
Formulabuilding lemma for use with the Distinctor Reduction Theorem.
Part of Theorem 9.4 of [Megill] p. 448 (p.
16 of preprint). (Contributed
by NM, 27Feb2005.)



Theorem  a4sbe 1609 
A specialization theorem, mostly the same as Theorem 19.8 of [Margaris]
p. 89. (Contributed by NM, 5Aug1993.) (Proof rewritten by Jim Kingdon,
29Dec2017.)



Theorem  a4sbim 1610 
Specialization of implication. (Contributed by NM, 5Aug1993.) (Proof
rewritten by Jim Kingdon, 21Jan2018.)



Theorem  a4sbbi 1611 
Specialization of biconditional. (Contributed by NM, 5Aug1993.) (Proof
rewritten by Jim Kingdon, 21Jan2018.)



Theorem  sbbid 1612 
Deduction substituting both sides of a biconditional. (Contributed by
NM, 5Aug1993.)



Theorem  sbequ8 1613 
Elimination of equality from antecedent after substitution. (Contributed
by NM, 5Aug1993.) (Proof revised by Jim Kingdon, 20Jan2018.)



Theorem  sbf3t 1614 
Substitution has no effect on a nonfree variable. (Contributed by NM,
30May2009.)



Theorem  sbid2 1615 
An identity law for substitution. (Contributed by NM, 5Aug1993.)



Theorem  sbidm 1616 
An idempotent law for substitution. (Contributed by NM, 30Jun1994.)
(Proof rewritten by Jim Kingdon, 21Jan2018.)



Theorem  sb5rf 1617 
Reversed substitution. (Contributed by NM, 3Feb2005.) (Proof
shortened by Andrew Salmon, 25May2011.)



Theorem  sb6rf 1618 
Reversed substitution. (Contributed by NM, 5Aug1993.) (Proof
shortened by Andrew Salmon, 25May2011.)



Theorem  sb8 1619 
Substitution of variable in universal quantifier. (Contributed by NM,
5Aug1993.) (Proof shortened by Andrew Salmon, 25May2011.) (Proof
shortened by Jim Kingdon, 15Jan2018.)



Theorem  sb8e 1620 
Substitution of variable in existential quantifier. (Contributed by NM,
12Aug1993.) (Proof rewritten by Jim Kingdon, 15Jan2018.)



1.4.4 Predicate calculus with distinct variables
(cont.)


Theorem  ax16i 1621* 
Inference with ax16 1581 as its conclusion, that doesn't require ax10 1329,
ax11 1330, or ax12 1335 for its proof. The hypotheses may be
eliminable
without one or more of these axioms in special cases. (Contributed by
NM, 20May2008.)



Theorem  ax16ALT 1622* 
Version of ax16 1580 that doesn't require ax10 1329 or ax12 1335 for its
proof. (Contributed by NM, 17May2008.)



Theorem  a4v 1623* 
Specialization, using implicit substitition. (Contributed by NM,
30Aug1993.)



Theorem  a4imev 1624* 
Distinctvariable version of a4ime 1514. (Contributed by NM,
5Aug1993.)



Theorem  a4eiv 1625* 
Inference from existential specialization, using implicit substitition.
(Contributed by NM, 19Aug1993.)



Theorem  equvin 1626* 
A variable introduction law for equality. Lemma 15 of [Monk2] p. 109.
(Contributed by NM, 5Aug1993.)



Theorem  a16g 1627* 
A generalization of axiom ax16 1581. (Contributed by NM, 5Aug1993.)
(Proof shortened by Andrew Salmon, 25May2011.)



Theorem  a16gb 1628* 
A generalization of axiom ax16 1581. (Contributed by NM, 5Aug1993.)



Theorem  a16nf 1629* 
If there is only one element in the universe, then everything satisfies
.
(Contributed by Mario Carneiro, 7Oct2016.)



Theorem  2albidv 1630* 
Formulabuilding rule for 2 existential quantifiers (deduction rule).
(Contributed by NM, 4Mar1997.)



Theorem  2exbidv 1631* 
Formulabuilding rule for 2 existential quantifiers (deduction rule).
(Contributed by NM, 1May1995.)



Theorem  3exbidv 1632* 
Formulabuilding rule for 3 existential quantifiers (deduction rule).
(Contributed by NM, 1May1995.)



Theorem  4exbidv 1633* 
Formulabuilding rule for 4 existential quantifiers (deduction rule).
(Contributed by NM, 3Aug1995.)



Theorem  19.9v 1634* 
Special case of Theorem 19.9 of [Margaris] p.
89. (Contributed by NM,
28May1995.) (Revised by NM, 21May2007.)



Theorem  19.21v 1635* 
Special case of Theorem 19.21 of [Margaris] p.
90. Notational
convention: We sometimes suffix with "v" the label of a
theorem
eliminating a hypothesis such as in 19.21 1380 via
the use of distinct variable conditions combined with ax17 1350.
Conversely, we sometimes suffix with "f" the label of a
theorem
introducing such a hypothesis to eliminate the need for the distinct
variable condition; e.g. euf 2081 derived from dfeu 2079. The "f" stands
for "not free in" which is less restrictive than "does
not occur in."
(Contributed by NM, 5Aug1993.)



Theorem  alrimiv 1636* 
Inference from Theorem 19.21 of [Margaris] p.
90. (Contributed by NM,
5Aug1993.)



Theorem  alrimivv 1637* 
Inference from Theorem 19.21 of [Margaris] p.
90. (Contributed by NM,
31Jul1995.)



Theorem  alrimdv 1638* 
Deduction from Theorem 19.21 of [Margaris] p.
90. (Contributed by NM,
10Feb1997.)



Theorem  nfdv 1639* 
Apply the definition of notfree in a context. (Contributed by Mario
Carneiro, 11Aug2016.)



Theorem  2ax17 1640* 
Quantification of two variables over a formula in which they do not
occur. (Contributed by Alan Sare, 12Apr2011.)



Theorem  alimdv 1641* 
Deduction from Theorem 19.20 of [Margaris] p.
90. (Contributed by NM,
3Apr1994.)



Theorem  eximdv 1642* 
Deduction from Theorem 19.22 of [Margaris] p.
90. (Contributed by NM,
27Apr1994.)



Theorem  2alimdv 1643* 
Deduction from Theorem 19.22 of [Margaris] p.
90. (Contributed by NM,
27Apr2004.)



Theorem  2eximdv 1644* 
Deduction from Theorem 19.22 of [Margaris] p.
90. (Contributed by NM,
3Aug1995.)



Theorem  19.23v 1645* 
Special case of Theorem 19.23 of [Margaris] p.
90. (Contributed by NM,
28Jun1998.)



Theorem  19.23vv 1646* 
Theorem 19.23 of [Margaris] p. 90 extended to
two variables.
(Contributed by NM, 10Aug2004.)



Theorem  sb56 1647* 
Two equivalent ways of expressing the proper substitution of for
in , when and are distinct. Theorem 6.2 of
[Quine] p. 40. The proof does not involve
dfsb 1533. (Contributed by
NM, 14Apr2008.)



Theorem  sb6 1648* 
Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40.
Also proved as Lemmas 16 and 17 of [Tarski] p. 70. (Contributed by NM,
18Aug1993.) (Revised by NM, 14Apr2008.)



Theorem  sb5 1649* 
Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40.
(Contributed by NM, 18Aug1993.) (Revised by NM, 14Apr2008.)



Theorem  sbnv 1650* 
Version of sbn 1703 where and are distinct. (Contributed by
Jim Kingdon, 18Dec2017.)



Theorem  sbanv 1651* 
Version of sban 1706 where and are distinct. (Contributed by
Jim Kingdon, 24Dec2017.)



Theorem  sborv 1652* 
Version of sbor 1705 where and are distinct. (Contributed by
Jim Kingdon, 3Feb2018.)



Theorem  sbi1v 1653* 
Forward direction of sbimv 1655. (Contributed by Jim Kingdon,
25Dec2017.)



Theorem  sbi2v 1654* 
Reverse direction of sbimv 1655. (Contributed by Jim Kingdon,
18Jan2018.)



Theorem  sbimv 1655* 
Intuitionistic proof of sbim 1704 where and are distinct.
(Contributed by Jim Kingdon, 18Jan2018.)



Theorem  sblimv 1656* 
Version of sblim 1708 where and are distinct. (Contributed by
Jim Kingdon, 19Jan2018.)



Theorem  pm11.53 1657* 
Theorem *11.53 in [WhiteheadRussell]
p. 164. (Contributed by Andrew
Salmon, 24May2011.)



Theorem  exlimivv 1658* 
Inference from Theorem 19.23 of [Margaris] p.
90. (Contributed by NM,
1Aug1995.)



Theorem  exlimdvv 1659* 
Deduction from Theorem 19.23 of [Margaris] p.
90. (Contributed by NM,
31Jul1995.)



Theorem  19.27v 1660* 
Theorem 19.27 of [Margaris] p. 90.
(Contributed by NM, 3Jun2004.)



Theorem  19.28v 1661* 
Theorem 19.28 of [Margaris] p. 90.
(Contributed by NM, 25Mar2004.)



Theorem  19.36aiv 1662* 
Inference from Theorem 19.36 of [Margaris] p.
90. (Contributed by NM,
5Aug1993.)



Theorem  19.41v 1663* 
Special case of Theorem 19.41 of [Margaris] p.
90. (Contributed by NM,
5Aug1993.)



Theorem  19.41vv 1664* 
Theorem 19.41 of [Margaris] p. 90 with 2
quantifiers. (Contributed by
NM, 30Apr1995.)



Theorem  19.41vvv 1665* 
Theorem 19.41 of [Margaris] p. 90 with 3
quantifiers. (Contributed by
NM, 30Apr1995.)



Theorem  19.41vvvv 1666* 
Theorem 19.41 of [Margaris] p. 90 with 4
quantifiers. (Contributed by
FL, 14Jul2007.)



Theorem  19.42v 1667* 
Special case of Theorem 19.42 of [Margaris] p.
90. (Contributed by NM,
5Aug1993.)



Theorem  exdistr 1668* 
Distribution of existential quantifiers. (Contributed by NM,
9Mar1995.)



Theorem  19.42vv 1669* 
Theorem 19.42 of [Margaris] p. 90 with 2
quantifiers. (Contributed by
NM, 16Mar1995.)



Theorem  19.42vvv 1670* 
Theorem 19.42 of [Margaris] p. 90 with 3
quantifiers. (Contributed by
NM, 21Sep2011.)



Theorem  exdistr2 1671* 
Distribution of existential quantifiers. (Contributed by NM,
17Mar1995.)



Theorem  3exdistr 1672* 
Distribution of existential quantifiers. (Contributed by NM,
9Mar1995.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  4exdistr 1673* 
Distribution of existential quantifiers. (Contributed by NM,
9Mar1995.)



Theorem  cbvalv 1674* 
Rule used to change bound variables, using implicit substitition.
(Contributed by NM, 5Aug1993.)



Theorem  cbvexv 1675* 
Rule used to change bound variables, using implicit substitition.
(Contributed by NM, 5Aug1993.)



Theorem  cbval2 1676* 
Rule used to change bound variables, using implicit substitition.
(Contributed by NM, 22Dec2003.)



Theorem  cbvex2 1677* 
Rule used to change bound variables, using implicit substitition.
(Contributed by NM, 14Sep2003.)



Theorem  cbval2v 1678* 
Rule used to change bound variables, using implicit substitition.
(Contributed by NM, 4Feb2005.)



Theorem  cbvex2v 1679* 
Rule used to change bound variables, using implicit substitition.
(Contributed by NM, 26Jul1995.)



Theorem  cbvald 1680* 
Deduction used to change bound variables, using implicit substitition,
particularly useful in conjunction with dvelim 1768. (Contributed by NM,
2Jan2002.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  cbvexd 1681* 
Deduction used to change bound variables, using implicit substitition,
particularly useful in conjunction with dvelim 1768. (Contributed by NM,
2Jan2002.) (Proof rewritten by Jim Kingdon, 30Dec2017.)



Theorem  cbvex4v 1682* 
Rule used to change bound variables, using implicit substitition.
(Contributed by NM, 26Jul1995.)



Theorem  eean 1683 
Rearrange existential quantifiers. (Contributed by NM, 27Oct2010.)



Theorem  eeanv 1684* 
Rearrange existential quantifiers. (Contributed by NM, 26Jul1995.)



Theorem  eeeanv 1685* 
Rearrange existential quantifiers. (Contributed by NM, 26Jul1995.)
(Proof shortened by Andrew Salmon, 25May2011.)



Theorem  ee4anv 1686* 
Rearrange existential quantifiers. (Contributed by NM, 31Jul1995.)



Theorem  nexdv 1687* 
Deduction for generalization rule for negated wff. (Contributed by NM,
5Aug1993.)



Theorem  chvarv 1688* 
Implicit substitution of for into a
theorem. (Contributed
by NM, 20Apr1994.)



Theorem  cleljust 1689* 
When the class variables of set theory are replaced with set variables,
this theorem of predicate calculus is the result. This theorem provides
part of the justification for the consistency of that definition, which
"overloads" the set variables in wel 1327
with the class variables in
wcel 1326. (Contributed by NM, 28Jan2004.)



1.4.5 More substitution theorems


Theorem  hbs1 1690* 
is not free in when and are
distinct. (Contributed by NM, 5Aug1993.) (Proof by Jim Kingdon,
16Dec2017.)



Theorem  nfs1v 1691* 
is not free in when and are
distinct. (Contributed by Mario Carneiro, 11Aug2016.)



Theorem  sbhb 1692* 
Two ways of expressing " is (effectively) not free in ."
(Contributed by NM, 29May2009.)



Theorem  sbhb2 1693* 
Two ways of expressing " is (effectively) not free in ."
(Contributed by Gérard Lang, 14Nov2013.)



Theorem  hbsbv 1694* 
This is a version of hbsb 1700 with an extra distinct variable constraint,
on and . (Contributed by Jim
Kingdon, 25Dec2017.)



Theorem  nfsbxy 1695* 
Similar to hbsb 1700 but with an extra distinct variable
constraint, on
and . (Contributed by Jim
Kingdon, 19Mar2018.)



Theorem  nfsbxyt 1696* 
Closed form of nfsbxy 1695. (Contributed by Jim Kingdon, 9May2018.)



Theorem  sbco2vlem 1697* 
This is a version of sbco2 1716 where is distinct from and from
. It is a lemma
on the way to proving sbco2v 1698 which only
requires that
and be distinct.
(Contributed by Jim Kingdon,
25Dec2017.) (One distinct variable constraint removed by Jim Kingdon,
3Feb2018.)



Theorem  sbco2v 1698* 
This is a version of sbco2 1716 where is distinct from .
(Contributed by Jim Kingdon, 12Feb2018.)



Theorem  nfsb 1699* 
If is not free in , it is not free in
when
and are distinct. (Contributed
by Mario Carneiro,
11Aug2016.) (Proof rewritten by Jim Kingdon, 19Mar2018.)



Theorem  hbsb 1700* 
If is not free in , it is not free in
when
and are distinct. (Contributed
by NM, 12Aug1993.) (Proof
rewritten by Jim Kingdon, 22Mar2018.)

