P. 333 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33201-33300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-19.23bit 33201	Closed form of 19.23bi 1814. (Contributed by BJ, 20-Oct-2019.)
|- ( ( E. x ph -> ps ) -> ( ph -> ps ) )
Theorem	bj-nexrt 33202	Closed form of nexr 1815. Contrapositive of 19.8a 1801. (Contributed by BJ, 20-Oct-2019.)
|- ( -. E. x ph -> -. ph )
Theorem	bj-alrim 33203	Closed form of alrimi 1820. (Contributed by BJ, 2-May-2019.)
|- ( F/ x ph -> ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) ) )
Theorem	bj-alrim2 33204	Imported form (uncurried form) of bj-alrim 33203. (Contributed by BJ, 2-May-2019.)
|- ( ( F/ x ph /\ A. x ( ph -> ps ) ) -> ( ph -> A. x ps ) )
Theorem	bj-nfdt0 33205	A theorem close to a closed form of nfd 1821 and nfdh 1822. (Contributed by BJ, 2-May-2019.)
|- ( A. x ( ph -> ( ps -> A. x ps ) ) -> ( A. x ph -> F/ x ps ) )
Theorem	bj-nfdt 33206	Closed form of nfd 1821 and nfdh 1822. (Contributed by BJ, 2-May-2019.)
|- ( A. x ( ph -> ( ps -> A. x ps ) ) -> ( ( ph -> A. x ph ) -> ( ph -> F/ x ps ) ) )
Theorem	bj-nexdt 33207	Closed form of nexd 1826. (Contributed by BJ, 20-Oct-2019.)
|- ( F/ x ph -> ( A. x ( ph -> -. ps ) -> ( ph -> -. E. x ps ) ) )
Theorem	bj-nexdvt 33208*	Closed form of nexdv 1827. (Contributed by BJ, 20-Oct-2019.)
|- ( A. x ( ph -> -. ps ) -> ( ph -> -. E. x ps ) )
Theorem	bj-19.3t 33209	Closed form of 19.3 1831. (Contributed by BJ, 20-Oct-2019.)
|- ( ( ph -> A. x ph ) -> ( A. x ph <-> ph ) )
Theorem	bj-alexbiex 33210	Adding a second quantifier is a tranparent operation, ( A. E. case). (Contributed by BJ, 20-Oct-2019.)
|- ( A. x E. x ph <-> E. x ph )
Theorem	bj-exexbiex 33211	Adding a second quantifier is a tranparent operation, ( E. E. case). (Contributed by BJ, 20-Oct-2019.)
|- ( E. x E. x ph <-> E. x ph )
Theorem	bj-alalbial 33212	Adding a second quantifier is a tranparent operation, ( A. A. case). (Contributed by BJ, 20-Oct-2019.)
|- ( A. x A. x ph <-> A. x ph )
Theorem	bj-exalbial 33213	Adding a second quantifier is a tranparent operation, ( E. A. case). (Contributed by BJ, 20-Oct-2019.)
|- ( E. x A. x ph <-> A. x ph )
Theorem	bj-19.9htbi 33214	Strengthening 19.9ht 1832 by replacing its succedent with a biconditional (19.9t 1833 does have a biconditional succedent). This propagates. (Contributed by BJ, 20-Oct-2019.)
|- ( A. x ( ph -> A. x ph ) -> ( E. x ph <-> ph ) )
Theorem	bj-hbntbi 33215	Strengthening hbnt 1837 by replacing its succedent with a biconditional. See also hbntg 28801 and hbntal 32281. (Contributed by BJ, 20-Oct-2019.) Proved from bj-19.9htbi 33214. (Proof modification is discouraged.)
|- ( A. x ( ph -> A. x ph ) -> ( -. ph <-> A. x -. ph ) )
Theorem	bj-biexal1 33216	A general FOL biconditional that generalizes 19.9ht 1832 among others. For this and the following theorems, see also 19.35 1659, 19.21 1848, 19.23 1852. (Contributed by BJ, 20-Oct-2019.)
|- ( A. x ( ph -> A. x ps ) <-> ( E. x ph -> A. x ps ) )
Theorem	bj-biexal2 33217	A general FOL biconditional. (Contributed by BJ, 20-Oct-2019.)
|- ( A. x ( E. x ph -> ps ) <-> ( E. x ph -> A. x ps ) )
Theorem	bj-biexal3 33218	A general FOL biconditional. (Contributed by BJ, 20-Oct-2019.)
|- ( A. x ( ph -> A. x ps ) <-> A. x ( E. x ph -> ps ) )
Theorem	bj-bialal 33219	A general FOL biconditional. (Contributed by BJ, 20-Oct-2019.)
|- ( A. x ( A. x ph -> ps ) <-> ( A. x ph -> A. x ps ) )
Theorem	bj-biexex 33220	A general FOL biconditional. (Contributed by BJ, 20-Oct-2019.)
|- ( A. x ( ph -> E. x ps ) <-> ( E. x ph -> E. x ps ) )
Theorem	bj-hbext 33221	Closed form of hbex 1888. (Contributed by BJ, 10-Oct-2019.)
|- ( A. y A. x ( ph -> A. x ph ) -> ( E. y ph -> A. x E. y ph ) )
Theorem	bj-nfalt 33222	Closed form of nfal 1889. (Contributed by BJ, 2-May-2019.)
|- ( A. x F/ y ph -> F/ y A. x ph )
Theorem	bj-nfext 33223	Closed form of nfex 1890. (Contributed by BJ, 10-Oct-2019.)
|- ( A. x F/ y ph -> F/ y E. x ph )
Theorem	bj-eeanvw 33224*	Version of eeanv 1950 with a DV condition on x , y not requiring ax-11 1786. (The same can be done with eeeanv 1951 and ee4anv 1952.) (Contributed by BJ, 29-Sep-2019.) (Proof modification is discouraged.)
|- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )
21.29.4.11  Adding ax-13
Theorem	bj-alequex 33225	A fol lemma. Can be used to reduce the proof of spimt 1967 from 133 to 112 bytes. (Contributed by BJ, 6-Oct-2018.)
|- ( A. x ( x = y -> ph ) -> E. x ph )
Theorem	bj-spimt2 33226	A step in the proof of spimt 1967. (Contributed by BJ, 2-May-2019.)
|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( ( E. x ps -> ps ) -> ( A. x ph -> ps ) ) )
Theorem	bj-cbv3ta 33227	Closed form of cbv3 1977. (Contributed by BJ, 2-May-2019.)
|- ( A. x A. y ( x = y -> ( ph -> ps ) ) -> ( ( A. y ( E. x ps -> ps ) /\ A. x ( ph -> A. y ph ) ) -> ( A. x ph -> A. y ps ) ) )
Theorem	bj-cbv3tb 33228	Closed form of cbv3 1977. (Contributed by BJ, 2-May-2019.)
|- ( A. x A. y ( x = y -> ( ph -> ps ) ) -> ( ( A. y F/ x ps /\ A. x F/ y ph ) -> ( A. x ph -> A. y ps ) ) )
Theorem	bj-hbsb3t 33229	A theorem close to a closed form of hbsb3 2069. (Contributed by BJ, 2-May-2019.)
|- ( A. x ( ph -> A. y ph ) -> ( [ y / x ] ph -> A. x [ y / x ] ph ) )
Theorem	bj-hbsb3 33230	Shorter proof of hbsb3 2069. (Contributed by BJ, 2-May-2019.)
|- ( ph -> A. y ph )   =>    |- ( [ y / x ] ph -> A. x [ y / x ] ph )
Theorem	bj-nfs1t 33231	A theorem close to a closed form of nfs1 2070. (Contributed by BJ, 2-May-2019.)
|- ( A. x ( ph -> A. y ph ) -> F/ x [ y / x ] ph )
Theorem	bj-nfs1t2 33232	A theorem close to a closed form of nfs1 2070. (Contributed by BJ, 2-May-2019.)
|- ( A. x F/ y ph -> F/ x [ y / x ] ph )
Theorem	bj-nfs1 33233	Shorter proof of nfs1 2070 (three essential steps instead of four). (Contributed by BJ, 2-May-2019.)
|- F/ y ph   =>    |- F/ x [ y / x ] ph
21.29.4.12  Removing dependencies on ax-13 (and ax-11) It is known that ax-13 1961 is logically redundant (see ax13w 1776 and the head comment of the section "Logical redundancy of ax-10--13"). More precisely, one can remove dependency on ax-13 1961 from every theorem in set.mm which is totally unbundled (i.e., has dv conditions on all setvar variables). Indeed, start with the existing proof, and replace any occurrence of ax-13 1961 with ax13w 1776. This section is an experiment to see in practice if (partially) unbundled versions of existing theorems can be proved more efficiently without ax-13 1961 (and using ax6v 1715 / ax6ev 1716 instead of ax-6 1714 / ax6e 1964, as is currently done). One reason to be optimistic is that the first few utility theorems using ax-13 1961 (roughly 200 of them) are then used mainly with dummy variables, which one can assume distinct from any other, so that the unbundled versions of the utility theorems suffice. In this section, we prove versions of theorems in the main part with dv conditions and not requiring ax-13 1961, labelled bj-xxxv (we follow the proof of xxx but use ax6v 1715 and ax6ev 1716 instead of ax-6 1714 and ax6e 1964, and ax-5 1675 instead of ax13v 1962; shorter proofs may be possible). When no additional dv condition is required, we label it bj-xxx. It is important to keep all the bundled theorems already in set.mm, but one may also add the (partially) unbundled versions which dipense with ax-13 1961, so as to remove dependencies on ax-13 1961 from many existing theorems. UPDATE: it turns out that several theorems of the form bj-xxxv, or minor variations, are already in set.mm with label xxxw. It is also possible to remove dependencies on ax-11 1786, typically by replacing a non-free hypothesis with a dv condition (see bj-cbv3v2 33246 and following theorems).
Theorem	bj-axc10v 33234*	Version of axc10 1966 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x ( x = y -> A. x ph ) -> ph )
Theorem	bj-spimtv 33235*	Version of spimt 1967 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
|- ( ( F/ x ps /\ A. x ( x = y -> ( ph -> ps ) ) ) -> ( A. x ph -> ps ) )
Theorem	bj-spimv 33236*	Version of spim 1968 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	bj-spimedv 33237*	Version of spimed 1969 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( ch -> F/ x ph )   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( ch -> ( ph -> E. x ps ) )
Theorem	bj-spimev 33238*	Version of spime 1970 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ x ph   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( ph -> E. x ps )
Theorem	bj-spimvv 33239*	Version of spimv 1971 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	bj-spimevv 33240*	Version of spimev 1972 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph -> ps ) )   =>    |- ( ph -> E. x ps )
Theorem	bj-spvv 33241*	Version of spv 1973 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	bj-speiv 33242*	Version of spei 1974 with a dv condition, which does not require ax-13 1961 (neither ax-7 1734 nor ax-12 1798). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ps   =>    |- E. x ph
Theorem	bj-chvarv 33243*	Version of chvar 1975 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	bj-chvarvv 33244*	Version of chvarv 1976 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	bj-cbv3v 33245*	Version of cbv3 1977 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> A. y ps )
Theorem	bj-cbv3v2 33246*	Version of cbv3 1977 with two dv conditions, which does not require ax-11 1786 nor ax-13 1961. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> A. y ps )
Theorem	bj-cbv3hv 33247*	Version of cbv3h 1978 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
|- ( ph -> A. y ph )   &    |- ( ps -> A. x ps )   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> A. y ps )
Theorem	bj-cbv3hv2 33248*	Version of cbv3h 1978 with two dv conditions, which does not require ax-11 1786 nor ax-13 1961. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( ps -> A. x ps )   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> A. y ps )
Theorem	bj-cbv1v 33249*	Version of cbv1 1979 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> F/ y ps )   &    |- ( ph -> F/ x ch )   &    |- ( ph -> ( x = y -> ( ps -> ch ) ) )   =>    |- ( ph -> ( A. x ps -> A. y ch ) )
Theorem	bj-cbv1hv 33250*	Version of cbv1h 1980 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ( ph -> ( ps -> A. y ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   &    |- ( ph -> ( x = y -> ( ps -> ch ) ) )   =>    |- ( A. x A. y ph -> ( A. x ps -> A. y ch ) )
Theorem	bj-cbv2hv 33251*	Version of cbv2h 1984 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ( ph -> ( ps -> A. y ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( A. x A. y ph -> ( A. x ps <-> A. y ch ) )
Theorem	bj-cbv2v 33252*	Version of cbv2 1985 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> F/ y ps )   &    |- ( ph -> F/ x ch )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( A. x ps <-> A. y ch ) )
Theorem	bj-cbvalv 33253*	Version of cbval 1987 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	bj-cbvexv 33254*	Version of cbvex 1988 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
Theorem	bj-cbvalvv 33255*	Version of cbvalv 1989 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	bj-cbvexvv 33256*	Version of cbvexv 1990 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
Theorem	bj-cbvaldv 33257*	Version of cbvald 1991 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- F/ y ph   &    |- ( ph -> F/ y ps )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( A. x ps <-> A. y ch ) )
Theorem	bj-cbvexdv 33258*	Version of cbvexd 1992 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- F/ y ph   &    |- ( ph -> F/ y ps )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( E. x ps <-> E. y ch ) )
Theorem	bj-cbval2v 33259*	Version of cbval2 1993 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- F/ z ph   &    |- F/ w ph   &    |- F/ x ps   &    |- F/ y ps   &    |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( A. x A. y ph <-> A. z A. w ps )
Theorem	bj-cbvex2v 33260*	Version of cbvex2 1994 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- F/ z ph   &    |- F/ w ph   &    |- F/ x ps   &    |- F/ y ps   &    |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( E. x E. y ph <-> E. z E. w ps )
Theorem	bj-cbval2vv 33261*	Version of cbval2v 1996 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( A. x A. y ph <-> A. z A. w ps )
Theorem	bj-cbvex2vv 33262*	Version of cbvex2v 1997 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( E. x E. y ph <-> E. z E. w ps )
Theorem	bj-cbvaldvav 33263*	Version of cbvaldva 1998 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x ps <-> A. y ch ) )
Theorem	bj-cbvexdvav 33264*	Version of cbvexdva 1999 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x ps <-> E. y ch ) )
Theorem	bj-cbvex4vv 33265*	Version of cbvex4v 2000 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ( ( x = v /\ y = u ) -> ( ph <-> ps ) )   &    |- ( ( z = f /\ w = g ) -> ( ps <-> ch ) )   =>    |- ( E. x E. y E. z E. w ph <-> E. v E. u E. f E. g ch )
Theorem	bj-equs4v 33266*	Version of equs4 2001 with a dv condition, which does not require ax-13 1961 (neither ax-5 1675 nor ax-7 1734 nor ax-12 1798). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x ( x = y -> ph ) -> E. x ( x = y /\ ph ) )
Theorem	bj-equsalv 33267*	Version of equsal 2002 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ( x = y -> ph ) <-> ps )
Theorem	bj-equsalhv 33268*	Version of equsalh 2003 with a dv condition, which does not require ax-13 1961. Remark: this is the same as equsalhw 1887. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
|- ( ps -> A. x ps )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ( x = y -> ph ) <-> ps )
Theorem	bj-equsexv 33269*	Version of equsex 2004 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ( x = y /\ ph ) <-> ps )
Theorem	bj-equsexhv 33270*	Version of equsexh 2005 with a dv condition, which does not require ax-13 1961. Remark: the theorem axc9lem2 2006 has a dv version which is a simple consequence of ax5e 1677; the theorems nfeqf2 2007, dveeq2 2008, nfeqf1 2009, dveeq1 2010, nfeqf 2011, axc9 2012, ax13 2013, have dv versions which are simple consequences of ax-5 1675. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( ps -> A. x ps )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ( x = y /\ ph ) <-> ps )
Theorem	bj-axc11nlemv 33271*	Version of axc11nlemOLD 2014 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x x = w -> A. y y = x )
Theorem	bj-axc11nv 33272*	Version of axc11n 2015 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> A. y y = x )
Theorem	bj-aecomsv 33273*	Version of aecoms 2018 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ph )   =>    |- ( A. y y = x -> ph )
Theorem	bj-naecomsv 33274*	Version of naecoms 2019 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ( -. A. x x = y -> ph )   =>    |- ( -. A. y y = x -> ph )
Theorem	bj-axc11v 33275*	Version of axc11 2020 with a dv condition, which does not require ax-13 1961. Remark: the following theorems (hbae 2021, nfae 2022, hbnae 2023, nfnae 2024, hbnaes 2025) would need to be totally unbundled to be proved without ax-13 1961, hence would be simple consequences of ax-5 1675 or nfv 1678. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
Theorem	bj-aevlem1v 33276*	Version of aevlem1 1881 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. z z = w -> A. y y = x )
Theorem	bj-axc16g 33277*	Remove dependency on ax-13 1961 from axc16g 1882. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ( ph -> A. z ph ) )
Theorem	bj-aev 33278*	Remove dependency on ax-13 1961 from aev 1885. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> A. z w = v )
Theorem	bj-axc16 33279*	Remove dependency on ax-13 1961 from axc16 1883. The same is doable for axc16i 2030 which has no interest. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ( ph -> A. x ph ) )
Theorem	bj-ax16nf 33280*	Remove dependency on ax-13 1961 from ax16nf 1886. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> F/ z ph )
Theorem	bj-ax16gb 33281*	Remove dependency on ax-13 1961 from ax16gb 1884. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ( ph <-> A. z ph ) )
Theorem	bj-dral1v 33282*	Version of dral1 2033 with a dv condition, which does not require ax-13 1961. Remark: the corresponding versions for dral2 2032 and drex2 2036 are instances of albidv 1684 and exbidv 1685 respectively. (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ( ph <-> ps ) )   =>    |- ( A. x x = y -> ( A. x ph <-> A. y ps ) )
Theorem	bj-drex1v 33283*	Version of drex1 2035 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ( ph <-> ps ) )   =>    |- ( A. x x = y -> ( E. x ph <-> E. y ps ) )
Theorem	bj-drnf1v 33284*	Version of drnf1 2037 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ( ph <-> ps ) )   =>    |- ( A. x x = y -> ( F/ x ph <-> F/ y ps ) )
Theorem	bj-drnf2v 33285*	Version of drnf2 2038 with a dv condition, which does not require ax-13 1961. Could be labelled "nfbidv". (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ( ph <-> ps ) )   =>    |- ( A. x x = y -> ( F/ z ph <-> F/ z ps ) )
Theorem	bj-axc15v 33286*	Version of axc15 2051 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
Theorem	bj-equs45fv 33287*	Version of equs45f 2057 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
|- F/ y ph   =>    |- ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) )
Theorem	bj-equs5v 33288*	Version of equs5 2058 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
|- ( -. A. x x = y -> ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) ) )
Theorem	bj-sb2v 33289*	Version of sb2 2059 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x ( x = y -> ph ) -> [ y / x ] ph )
Theorem	bj-stdpc4v 33290*	Version of stdpc4 2060 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x ph -> [ y / x ] ph )
Theorem	bj-2stdpc4v 33291*	Version of 2stdpc4 2061 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x A. y ph -> [ z / x ] [ w / y ] ph )
Theorem	bj-sb3v 33292*	Version of sb3 2062 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( -. A. x x = y -> ( E. x ( x = y /\ ph ) -> [ y / x ] ph ) )
Theorem	bj-sb4v 33293*	Version of sb4 2063 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( -. A. x x = y -> ( [ y / x ] ph -> A. x ( x = y -> ph ) ) )
Theorem	bj-sb4bv 33294*	Version of sb4b 2064 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( -. A. x x = y -> ( [ y / x ] ph <-> A. x ( x = y -> ph ) ) )
Theorem	bj-hbsb2v 33295*	Version of hbsb2 2065 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( -. A. x x = y -> ( [ y / x ] ph -> A. x [ y / x ] ph ) )
Theorem	bj-nfsb2v 33296*	Version of nfsb2 2066 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( -. A. x x = y -> F/ x [ y / x ] ph )
Theorem	bj-hbsb2av 33297*	Version of hbsb2a 2067 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
|- ( [ y / x ] A. y ph -> A. x [ y / x ] ph )
Theorem	bj-hbsb3v 33298*	Version of hbsb3 2069 with a dv condition, which does not require ax-13 1961. (Remark: the unbundled version of nfs1 2070 is given by bj-nfs1v 33309.) (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
|- ( ph -> A. y ph )   =>    |- ( [ y / x ] ph -> A. x [ y / x ] ph )
Theorem	bj-equsb1v 33299*	Version of equsb1 2073 with a dv condition, which does not require ax-13 1961. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
|- [ y / x ] x = y
Theorem	bj-cleljust 33300*	Remove dependency on ax-13 1961 from cleljust 2075. (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.)
|- ( x e. y <-> E. z ( z = x /\ z e. y ) )