Type  Label  Description 
Statement 

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



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



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



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



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



Theorem  19.42vvvv 1806* 
Theorem 19.42 of [Margaris] p. 90 with 4
quantifiers. (Contributed by
Jim Kingdon, 23Nov2019.)



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



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



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



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



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



Theorem  cbval2 1812* 
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 22Dec2003.) (Revised by Mario Carneiro,
6Oct2016.) (Proof shortened by Wolf Lammen, 22Apr2018.)



Theorem  cbvex2 1813* 
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 14Sep2003.) (Revised by Mario Carneiro,
6Oct2016.)



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



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



Theorem  cbvald 1816* 
Deduction used to change bound variables, using implicit substitution,
particularly useful in conjunction with dvelim 1909. (Contributed by NM,
2Jan2002.) (Revised by Mario Carneiro, 6Oct2016.) (Revised by Wolf
Lammen, 13May2018.)



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



Theorem  cbvexd 1818* 
Deduction used to change bound variables, using implicit substitution,
particularly useful in conjunction with dvelim 1909. (Contributed by NM,
2Jan2002.) (Revised by Mario Carneiro, 6Oct2016.) (Proof rewritten
by Jim Kingdon, 10Jun2018.)



Theorem  cbvaldva 1819* 
Rule used to change the bound variable in a universal quantifier with
implicit substitution. Deduction form. (Contributed by David Moews,
1May2017.)



Theorem  cbvexdva 1820* 
Rule used to change the bound variable in an existential quantifier with
implicit substitution. Deduction form. (Contributed by David Moews,
1May2017.)



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



Theorem  eean 1822 
Rearrange existential quantifiers. (Contributed by NM, 27Oct2010.)
(Revised by Mario Carneiro, 6Oct2016.)



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



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



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



Theorem  ee8anv 1826* 
Rearrange existential quantifiers. (Contributed by Jim Kingdon,
23Nov2019.)



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



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



Theorem  cleljust 1829* 
When the class variables of set theory are replaced with setvar
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 setvar variables in wel 1410
with the
class variables in wcel 1409. (Contributed by NM, 28Jan2004.)



1.4.5 More substitution theorems


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



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



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



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



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



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



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



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



Theorem  nfsb 1838* 
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 1839* 
If is not free in , it is not free in
when
and are distinct. (Contributed
by NM, 12Aug1993.) (Proof
rewritten by Jim Kingdon, 22Mar2018.)



Theorem  equsb3lem 1840* 
Lemma for equsb3 1841. (Contributed by NM, 4Dec2005.) (Proof
shortened
by Andrew Salmon, 14Jun2011.)



Theorem  equsb3 1841* 
Substitution applied to an atomic wff. (Contributed by Raph Levien and
FL, 4Dec2005.)



Theorem  sbn 1842 
Negation inside and outside of substitution are equivalent.
(Contributed by NM, 5Aug1993.) (Proof rewritten by Jim Kingdon,
3Feb2018.)



Theorem  sbim 1843 
Implication inside and outside of substitution are equivalent.
(Contributed by NM, 5Aug1993.) (Proof rewritten by Jim Kingdon,
3Feb2018.)



Theorem  sbor 1844 
Logical OR inside and outside of substitution are equivalent.
(Contributed by NM, 29Sep2002.) (Proof rewritten by Jim Kingdon,
3Feb2018.)



Theorem  sban 1845 
Conjunction inside and outside of a substitution are equivalent.
(Contributed by NM, 5Aug1993.) (Proof rewritten by Jim Kingdon,
3Feb2018.)



Theorem  sbrim 1846 
Substitution with a variable not free in antecedent affects only the
consequent. (Contributed by NM, 5Aug1993.)



Theorem  sblim 1847 
Substitution with a variable not free in consequent affects only the
antecedent. (Contributed by NM, 14Nov2013.) (Revised by Mario
Carneiro, 4Oct2016.)



Theorem  sb3an 1848 
Conjunction inside and outside of a substitution are equivalent.
(Contributed by NM, 14Dec2006.)



Theorem  sbbi 1849 
Equivalence inside and outside of a substitution are equivalent.
(Contributed by NM, 5Aug1993.)



Theorem  sblbis 1850 
Introduce left biconditional inside of a substitution. (Contributed by
NM, 19Aug1993.)



Theorem  sbrbis 1851 
Introduce right biconditional inside of a substitution. (Contributed by
NM, 18Aug1993.)



Theorem  sbrbif 1852 
Introduce right biconditional inside of a substitution. (Contributed by
NM, 18Aug1993.)



Theorem  sbco2yz 1853* 
This is a version of sbco2 1855 where is distinct from . It is
a lemma on the way to proving sbco2 1855 which has no distinct variable
constraints. (Contributed by Jim Kingdon, 19Mar2018.)



Theorem  sbco2h 1854 
A composition law for substitution. (Contributed by NM, 30Jun1994.)
(Proof rewritten by Jim Kingdon, 19Mar2018.)



Theorem  sbco2 1855 
A composition law for substitution. (Contributed by NM, 30Jun1994.)
(Revised by Mario Carneiro, 6Oct2016.)



Theorem  sbco2d 1856 
A composition law for substitution. (Contributed by NM, 5Aug1993.)



Theorem  sbco2vd 1857* 
Version of sbco2d 1856 with a distinct variable constraint between
and .
(Contributed by Jim Kingdon, 19Feb2018.)



Theorem  sbco 1858 
A composition law for substitution. (Contributed by NM, 5Aug1993.)



Theorem  sbco3v 1859* 
Version of sbco3 1864 with a distinct variable constraint between
and
. (Contributed
by Jim Kingdon, 19Feb2018.)



Theorem  sbcocom 1860 
Relationship between composition and commutativity for substitution.
(Contributed by Jim Kingdon, 28Feb2018.)



Theorem  sbcomv 1861* 
Version of sbcom 1865 with a distinct variable constraint between
and
. (Contributed
by Jim Kingdon, 28Feb2018.)



Theorem  sbcomxyyz 1862* 
Version of sbcom 1865 with distinct variable constraints between
and
, and and . (Contributed by Jim Kingdon,
21Mar2018.)



Theorem  sbco3xzyz 1863* 
Version of sbco3 1864 with distinct variable constraints between
and
, and and . Lemma for proving sbco3 1864. (Contributed
by Jim Kingdon, 22Mar2018.)



Theorem  sbco3 1864 
A composition law for substitution. (Contributed by NM, 5Aug1993.)
(Proof rewritten by Jim Kingdon, 22Mar2018.)



Theorem  sbcom 1865 
A commutativity law for substitution. (Contributed by NM, 27May1997.)
(Proof rewritten by Jim Kingdon, 22Mar2018.)



Theorem  nfsbt 1866* 
Closed form of nfsb 1838. (Contributed by Jim Kingdon, 9May2018.)



Theorem  nfsbd 1867* 
Deduction version of nfsb 1838. (Contributed by NM, 15Feb2013.)



Theorem  elsb3 1868* 
Substitution applied to an atomic membership wff. (Contributed by NM,
7Nov2006.) (Proof shortened by Andrew Salmon, 14Jun2011.)



Theorem  elsb4 1869* 
Substitution applied to an atomic membership wff. (Contributed by
Rodolfo Medina, 3Apr2010.) (Proof shortened by Andrew Salmon,
14Jun2011.)



Theorem  sb9v 1870* 
Like sb9 1871 but with a distinct variable constraint
between and
. (Contributed
by Jim Kingdon, 28Feb2018.)



Theorem  sb9 1871 
Commutation of quantification and substitution variables. (Contributed
by NM, 5Aug1993.) (Proof rewritten by Jim Kingdon, 23Mar2018.)



Theorem  sb9i 1872 
Commutation of quantification and substitution variables. (Contributed by
NM, 5Aug1993.) (Proof rewritten by Jim Kingdon, 23Mar2018.)



Theorem  sbnf2 1873* 
Two ways of expressing " is (effectively) not free in ."
(Contributed by Gérard Lang, 14Nov2013.) (Revised by Mario
Carneiro, 6Oct2016.)



Theorem  hbsbd 1874* 
Deduction version of hbsb 1839. (Contributed by NM, 15Feb2013.) (Proof
rewritten by Jim Kingdon, 23Mar2018.)



Theorem  2sb5 1875* 
Equivalence for double substitution. (Contributed by NM,
3Feb2005.)



Theorem  2sb6 1876* 
Equivalence for double substitution. (Contributed by NM,
3Feb2005.)



Theorem  sbcom2v 1877* 
Lemma for proving sbcom2 1879. It is the same as sbcom2 1879 but with
additional distinct variable constraints on and , and on
and . (Contributed by Jim
Kingdon, 19Feb2018.)



Theorem  sbcom2v2 1878* 
Lemma for proving sbcom2 1879. It is the same as sbcom2v 1877 but removes
the distinct variable constraint on and . (Contributed by
Jim Kingdon, 19Feb2018.)



Theorem  sbcom2 1879* 
Commutativity law for substitution. Used in proof of Theorem 9.7 of
[Megill] p. 449 (p. 16 of the preprint).
(Contributed by NM,
27May1997.) (Proof modified to be intuitionistic by Jim Kingdon,
19Feb2018.)



Theorem  sb6a 1880* 
Equivalence for substitution. (Contributed by NM, 5Aug1993.)



Theorem  2sb5rf 1881* 
Reversed double substitution. (Contributed by NM, 3Feb2005.)



Theorem  2sb6rf 1882* 
Reversed double substitution. (Contributed by NM, 3Feb2005.)



Theorem  dfsb7 1883* 
An alternate definition of proper substitution dfsb 1662. By introducing
a dummy variable
in the definiens, we are able to eliminate any
distinct variable restrictions among the variables , , and
of the
definiendum. No distinct variable conflicts arise because
effectively
insulates from . To achieve this, we use
a chain of two substitutions in the form of sb5 1783,
first for
then for . Compare Definition 2.1'' of [Quine] p. 17.
Theorem sb7f 1884 provides a version where and don't have to
be distinct. (Contributed by NM, 28Jan2004.)



Theorem  sb7f 1884* 
This version of dfsb7 1883 does not require that and be
distinct. This permits it to be used as a definition for substitution
in a formalization that omits the logically redundant axiom ax17 1435 i.e.
that doesn't have the concept of a variable not occurring in a wff.
(dfsb 1662 is also suitable, but its mixing of free and
bound variables
is distasteful to some logicians.) (Contributed by NM, 26Jul2006.)
(Proof shortened by Andrew Salmon, 25May2011.)



Theorem  sb7af 1885* 
An alternative definition of proper substitution dfsb 1662. Similar to
dfsb7a 1886 but does not require that and be distinct.
Similar to sb7f 1884 in that it involves a dummy variable , but
expressed in terms of rather than . (Contributed by Jim
Kingdon, 5Feb2018.)



Theorem  dfsb7a 1886* 
An alternative definition of proper substitution dfsb 1662. Similar to
dfsb7 1883 in that it involves a dummy variable , but expressed in
terms of
rather than . For
a version which only requires
rather than and being distinct, see sb7af 1885.
(Contributed by Jim Kingdon, 5Feb2018.)



Theorem  sb10f 1887* 
Hao Wang's identity axiom P6 in Irving Copi, Symbolic Logic (5th ed.,
1979), p. 328. In traditional predicate calculus, this is a sole axiom
for identity from which the usual ones can be derived. (Contributed by
NM, 9May2005.)



Theorem  sbid2v 1888* 
An identity law for substitution. Used in proof of Theorem 9.7 of
[Megill] p. 449 (p. 16 of the preprint).
(Contributed by NM,
5Aug1993.)



Theorem  sbelx 1889* 
Elimination of substitution. (Contributed by NM, 5Aug1993.)



Theorem  sbel2x 1890* 
Elimination of double substitution. (Contributed by NM, 5Aug1993.)



Theorem  sbalyz 1891* 
Move universal quantifier in and out of substitution. Identical to
sbal 1892 except that it has an additional distinct
variable constraint on
and . (Contributed by Jim
Kingdon, 29Dec2017.)



Theorem  sbal 1892* 
Move universal quantifier in and out of substitution. (Contributed by
NM, 5Aug1993.) (Proof rewritten by Jim Kingdon, 12Feb2018.)



Theorem  sbal1yz 1893* 
Lemma for proving sbal1 1894. Same as sbal1 1894 but with an additional
distinct variable constraint on and . (Contributed by Jim
Kingdon, 23Feb2018.)



Theorem  sbal1 1894* 
A theorem used in elimination of disjoint variable restriction on
and by replacing
it with a distinctor .
(Contributed by NM, 5Aug1993.) (Proof rewitten by Jim Kingdon,
24Feb2018.)



Theorem  sbexyz 1895* 
Move existential quantifier in and out of substitution. Identical to
sbex 1896 except that it has an additional distinct
variable constraint on
and . (Contributed by Jim
Kingdon, 29Dec2017.)



Theorem  sbex 1896* 
Move existential quantifier in and out of substitution. (Contributed by
NM, 27Sep2003.) (Proof rewritten by Jim Kingdon, 12Feb2018.)



Theorem  sbalv 1897* 
Quantify with new variable inside substitution. (Contributed by NM,
18Aug1993.)



Theorem  sbco4lem 1898* 
Lemma for sbco4 1899. It replaces the temporary variable with
another temporary variable . (Contributed by Jim Kingdon,
26Sep2018.)



Theorem  sbco4 1899* 
Two ways of exchanging two variables. Both sides of the biconditional
exchange and
, either via two
temporary variables
and
, or a single
temporary .
(Contributed by Jim Kingdon,
25Sep2018.)



Theorem  exsb 1900* 
An equivalent expression for existence. (Contributed by NM,
2Feb2005.)

