P. 334 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33301-33400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-alrimhi 33301	An inference associated with bj-alrimh 33296 and bj-exlimh 33299. (Contributed by BJ, 12-May-2019.)
|- ( ph -> ps )   =>    |- (FF/ x ph -> ( E. x ph -> A. x ps ) )
Theorem	bj-nexdh 33302	Closed form of nexdh 1651 (and more general since it uses ch). (Contributed by BJ, 6-May-2019.)
|- ( A. x ( ph -> -. ps ) -> ( ( ch -> A. x ph ) -> ( ch -> -. E. x ps ) ) )
Theorem	bj-nexdh2 33303	Uncurried form of bj-nexdh 33302. (Contributed by BJ, 6-May-2019.)
|- ( ( A. x ( ph -> -. ps ) /\ ( ch -> A. x ph ) ) -> ( ch -> -. E. x ps ) )
Theorem	bj-hbxfrbi 33304	Closed form of hbxfrbi 1623. Notes: it is less important than bj-nfbi 33305; it requires sp 1808 (unlike bj-nfbi 33305); there is an obvious version with ( E. x ph -> ph ) instead. (Contributed by BJ, 6-May-2019.)
|- ( A. x ( ph <-> ps ) -> ( ( ph -> A. x ph ) <-> ( ps -> A. x ps ) ) )
Theorem	bj-nfbi 33305	Closed form of nfbii 1624 (with df-bj-nf 33278 instead of df-nf 1600, which would require more axioms). (Contributed by BJ, 6-May-2019.)
|- ( A. x ( ph <-> ps ) -> (FF/ x ph <-> FF/ x ps ) )
Theorem	bj-nfxfr 33306	Proof of nfxfr 1625 from bj-nfbi 33305. (Contributed by BJ, 6-May-2019.)
|- ( ph <-> ps )   &    |- FF/ x ph   =>    |- FF/ x ps
Theorem	bj-nfn 33307	A variable is non-free in a proposition if and only if it is so in its negation. Requires fewer axioms than nfn 1849. (Contributed by BJ, 6-May-2019.)
|- (FF/ x ph <-> FF/ x -. ph )
Theorem	bj-19.40b 33308	The antecedent provides a condition implying the converse of 19.40 1656. This is to 19.40 1656 what 19.33b 1673 is to 19.33 1672. (Contributed by BJ, 6-May-2019.)
|- ( ( A. x ph \/ A. x ps ) -> ( ( E. x ph /\ E. x ps ) <-> E. x ( ph /\ ps ) ) )
21.29.4.4  Adding ax-5
Theorem	bj-nfv 33309*	A non-occurring variable is semantically non-free. (Contributed by BJ, 6-May-2019.)
|- FF/ x ph
21.29.4.5  Equality and substitution The following theorems are the general instances of already proved theorems. They could be moved to the main part, right before weq 1705. I propose to move to the main part: bj-exnalimn 33310, bj-exaleximi 33313, bj-exalimi 33314, bj-ax12i 33315. A new label is needed for bj-ax12i 33315 and label suggestions are welcome for the others. I also propose to change -. A. x -. to E. x in speimfw 1707 and spimfw 1709 (other spim* theorems use E. x and very very few theorems in set.mm use -. A. x -.).
Theorem	bj-exnalimn 33310	A transformation of quantifiers and logical connectives. The general statement that equs3 1706 proves. (Contributed by BJ, 29-Sep-2019.)
|- ( E. x ( ph /\ ps ) <-> -. A. x ( ph -> -. ps ) )
Theorem	bj-nalnaleximiOLD 33311	An inference for distributing quantifiers over a double implication. The general statement that speimfw 1707 proves. (Contributed by BJ, 12-May-2019.)
|- ( ch -> ( ph -> ps ) )   =>    |- ( -. A. x -. ch -> ( A. x ph -> E. x ps ) )
Theorem	bj-nalnalimiOLD 33312	An inference for distributing quantifiers over a double implication. The general statement that spimfw 1709 proves. (Contributed by BJ, 12-May-2019.)
|- ( ch -> ( ph -> ps ) )   &    |- ( -. ps -> A. x -. ps )   =>    |- ( -. A. x -. ch -> ( A. x ph -> ps ) )
Theorem	bj-exaleximi 33313	An inference for distributing quantifiers over a double implication. (Almost) the general statement that speimfw 1707 proves. (Contributed by BJ, 29-Sep-2019.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( E. x ph -> ( A. x ps -> E. x ch ) )
Theorem	bj-exalimi 33314	An inference for distributing quantifiers over a double implication. (Almost) the general statement that spimfw 1709 proves. (Contributed by BJ, 29-Sep-2019.)
|- ( ph -> ( ps -> ch ) )   &    |- ( E. x ph -> ( -. ch -> A. x -. ch ) )   =>    |- ( E. x ph -> ( A. x ps -> ch ) )
Theorem	bj-ax12i 33315	A statement close to the axiom of substitution ax-12 1803. (Almost) the general statement that ax12i 1710 proves. (Contributed by BJ, 29-Sep-2019.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ch -> A. x ch )   =>    |- ( ph -> ( ps -> A. x ( ph -> ps ) ) )
21.29.4.6  Adding ax-6
Theorem	bj-19.8w 33316	The general statement that 19.8w 1724 proves (deduction form of 19.2 1723, so could be labelled 19.2d instead). (Contributed by BJ, 12-May-2019.)
|- ( ph -> A. x ps )   =>    |- ( ph -> E. x ps )
Theorem	bj-spnfw 33317	Theorem close to a closed form of spnfw 1734. (Contributed by BJ, 12-May-2019.)
|- ( ( E. x ph -> ps ) -> ( A. x ph -> ps ) )
21.29.4.7  Adding ax-7
Theorem	bj-equcomd 33318	Deduction form of equcom 1743, symmetry of equality. For the versions for classes, see eqcom 2476 and eqcomd 2475. (TODO: move to main part.) (Contributed by BJ, 6-Oct-2019.)
|- ( ph -> x = y )   =>    |- ( ph -> y = x )
21.29.4.8  Membership predicate, ax-8 and ax-9
Theorem	bj-elequ2g 33319*	A form of elequ2 1772 with a universal quantifier. Its converse is ax-ext 2445. (TODO: move to main part, minimize axext4 2449.) (Contributed by BJ, 3-Oct-2019.)
|- ( x = y -> A. z ( z e. x <-> z e. y ) )
Theorem	bj-ax89 33320	A theorem which could be used as sole axiom for the non-logical predicate instead of ax-8 1769 and ax-9 1771. Indeed, it is implied over propositional calculus by the conjunction of ax-8 1769 and ax-9 1771, as proved here. In the other direction, one can prove ax-8 1769 (respectively ax-9 1771) from bj-ax89 33320 by using mpan2 671 ( respectively mpan 670) and equid 1740. (TODO: move to main part.) (Contributed by BJ, 3-Oct-2019.)
|- ( ( x = y /\ z = t ) -> ( x e. z -> y e. t ) )
Theorem	bj-elequ12 33321	An identity law for the non-logical predicate, which combines elequ1 1770 and elequ2 1772. For the analogous theorems for class terms, see eleq1 2539, eleq2 2540 and eleq12 2543. (TODO: move to main part.) (Contributed by BJ, 29-Sep-2019.)
|- ( ( x = y /\ z = t ) -> ( x e. z <-> y e. t ) )
21.29.4.9  Adding ax-11
Theorem	bj-hbalt 33322	Closed form of hbal 1793. When in main part, prove hbal 1793 and hbald 1797 from it. (Contributed by BJ, 2-May-2019.)
|- ( A. y ( ph -> A. x ph ) -> ( A. y ph -> A. x A. y ph ) )
21.29.4.10  Adding ax-12
Theorem	bj-modalbe 33323	The predicate-calculus version of the axiom (B) of modal logic. See also modal-b 1812. (Contributed by BJ, 20-Oct-2019.)
|- ( ph -> A. x E. x ph )
Theorem	bj-spst 33324	Closed form of sps 1814. Once in main part, prove sps 1814 and spsd 1816 from it. (Contributed by BJ, 20-Oct-2019.)
|- ( ( ph -> ps ) -> ( A. x ph -> ps ) )
Theorem	bj-19.21bit 33325	Closed form of 19.21bi 1818. (Contributed by BJ, 20-Oct-2019.)
|- ( ( ph -> A. x ps ) -> ( ph -> ps ) )
Theorem	bj-19.23bit 33326	Closed form of 19.23bi 1819. (Contributed by BJ, 20-Oct-2019.)
|- ( ( E. x ph -> ps ) -> ( ph -> ps ) )
Theorem	bj-nexrt 33327	Closed form of nexr 1820. Contrapositive of 19.8a 1806. (Contributed by BJ, 20-Oct-2019.)
|- ( -. E. x ph -> -. ph )
Theorem	bj-alrim 33328	Closed form of alrimi 1825. (Contributed by BJ, 2-May-2019.)
|- ( F/ x ph -> ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) ) )
Theorem	bj-alrim2 33329	Imported form (uncurried form) of bj-alrim 33328. (Contributed by BJ, 2-May-2019.)
|- ( ( F/ x ph /\ A. x ( ph -> ps ) ) -> ( ph -> A. x ps ) )
Theorem	bj-nfdt0 33330	A theorem close to a closed form of nfd 1826 and nfdh 1827. (Contributed by BJ, 2-May-2019.)
|- ( A. x ( ph -> ( ps -> A. x ps ) ) -> ( A. x ph -> F/ x ps ) )
Theorem	bj-nfdt 33331	Closed form of nfd 1826 and nfdh 1827. (Contributed by BJ, 2-May-2019.)
|- ( A. x ( ph -> ( ps -> A. x ps ) ) -> ( ( ph -> A. x ph ) -> ( ph -> F/ x ps ) ) )
Theorem	bj-nexdt 33332	Closed form of nexd 1831. (Contributed by BJ, 20-Oct-2019.)
|- ( F/ x ph -> ( A. x ( ph -> -. ps ) -> ( ph -> -. E. x ps ) ) )
Theorem	bj-nexdvt 33333*	Closed form of nexdv 1832. (Contributed by BJ, 20-Oct-2019.)
|- ( A. x ( ph -> -. ps ) -> ( ph -> -. E. x ps ) )
Theorem	bj-19.3t 33334	Closed form of 19.3 1836. (Contributed by BJ, 20-Oct-2019.)
|- ( ( ph -> A. x ph ) -> ( A. x ph <-> ph ) )
Theorem	bj-alexbiex 33335	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 33336	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 33337	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 33338	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 33339	Strengthening 19.9ht 1837 by replacing its succedent with a biconditional (19.9t 1838 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 33340	Strengthening hbnt 1842 by replacing its succedent with a biconditional. See also hbntg 28815 and hbntal 32406. (Contributed by BJ, 20-Oct-2019.) Proved from bj-19.9htbi 33339. (Proof modification is discouraged.)
|- ( A. x ( ph -> A. x ph ) -> ( -. ph <-> A. x -. ph ) )
Theorem	bj-biexal1 33341	A general FOL biconditional that generalizes 19.9ht 1837 among others. For this and the following theorems, see also 19.35 1664, 19.21 1853, 19.23 1857. (Contributed by BJ, 20-Oct-2019.)
|- ( A. x ( ph -> A. x ps ) <-> ( E. x ph -> A. x ps ) )
Theorem	bj-biexal2 33342	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 33343	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 33344	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 33345	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 33346	Closed form of hbex 1893. (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 33347	Closed form of nfal 1894. (Contributed by BJ, 2-May-2019.)
|- ( A. x F/ y ph -> F/ y A. x ph )
Theorem	bj-nfext 33348	Closed form of nfex 1895. (Contributed by BJ, 10-Oct-2019.)
|- ( A. x F/ y ph -> F/ y E. x ph )
Theorem	bj-eeanvw 33349*	Version of eeanv 1957 with a DV condition on x , y not requiring ax-11 1791. (The same can be done with eeeanv 1958 and ee4anv 1959.) (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 33350	A fol lemma. Can be used to reduce the proof of spimt 1974 from 133 to 112 bytes. (Contributed by BJ, 6-Oct-2018.)
|- ( A. x ( x = y -> ph ) -> E. x ph )
Theorem	bj-spimt2 33351	A step in the proof of spimt 1974. (Contributed by BJ, 2-May-2019.)
|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( ( E. x ps -> ps ) -> ( A. x ph -> ps ) ) )
Theorem	bj-cbv3ta 33352	Closed form of cbv3 1984. (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 33353	Closed form of cbv3 1984. (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 33354	A theorem close to a closed form of hbsb3 2076. (Contributed by BJ, 2-May-2019.)
|- ( A. x ( ph -> A. y ph ) -> ( [ y / x ] ph -> A. x [ y / x ] ph ) )
Theorem	bj-hbsb3 33355	Shorter proof of hbsb3 2076. (Contributed by BJ, 2-May-2019.)
|- ( ph -> A. y ph )   =>    |- ( [ y / x ] ph -> A. x [ y / x ] ph )
Theorem	bj-nfs1t 33356	A theorem close to a closed form of nfs1 2077. (Contributed by BJ, 2-May-2019.)
|- ( A. x ( ph -> A. y ph ) -> F/ x [ y / x ] ph )
Theorem	bj-nfs1t2 33357	A theorem close to a closed form of nfs1 2077. (Contributed by BJ, 2-May-2019.)
|- ( A. x F/ y ph -> F/ x [ y / x ] ph )
Theorem	bj-nfs1 33358	Shorter proof of nfs1 2077 (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 1968 is logically redundant (see ax13w 1781 and the head comment of the section "Logical redundancy of ax-10--13"). More precisely, one can remove dependency on ax-13 1968 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 1968 with ax13w 1781. This section is an experiment to see in practice if (partially) unbundled versions of existing theorems can be proved more efficiently without ax-13 1968 (and using ax6v 1720 / ax6ev 1721 instead of ax-6 1719 / ax6e 1971, as is currently done). One reason to be optimistic is that the first few utility theorems using ax-13 1968 (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 1968, labelled bj-xxxv (we follow the proof of xxx but use ax6v 1720 and ax6ev 1721 instead of ax-6 1719 and ax6e 1971, and ax-5 1680 instead of ax13v 1969; 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 1968, so as to remove dependencies on ax-13 1968 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 1791, typically by replacing a non-free hypothesis with a dv condition (see bj-cbv3v2 33371 and following theorems).
Theorem	bj-axc10v 33359*	Version of axc10 1973 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x ( x = y -> A. x ph ) -> ph )
Theorem	bj-spimtv 33360*	Version of spimt 1974 with a dv condition, which does not require ax-13 1968. (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 33361*	Version of spim 1975 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	bj-spimedv 33362*	Version of spimed 1976 with a dv condition, which does not require ax-13 1968. (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 33363*	Version of spime 1977 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ x ph   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( ph -> E. x ps )
Theorem	bj-spimvv 33364*	Version of spimv 1978 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	bj-spimevv 33365*	Version of spimev 1979 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph -> ps ) )   =>    |- ( ph -> E. x ps )
Theorem	bj-spvv 33366*	Version of spv 1980 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	bj-speiv 33367*	Version of spei 1981 with a dv condition, which does not require ax-13 1968 (neither ax-7 1739 nor ax-12 1803). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ps   =>    |- E. x ph
Theorem	bj-chvarv 33368*	Version of chvar 1982 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	bj-chvarvv 33369*	Version of chvarv 1983 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	bj-cbv3v 33370*	Version of cbv3 1984 with a dv condition, which does not require ax-13 1968. (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 33371*	Version of cbv3 1984 with two dv conditions, which does not require ax-11 1791 nor ax-13 1968. (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 33372*	Version of cbv3h 1985 with a dv condition, which does not require ax-13 1968. (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 33373*	Version of cbv3h 1985 with two dv conditions, which does not require ax-11 1791 nor ax-13 1968. (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 33374*	Version of cbv1 1986 with a dv condition, which does not require ax-13 1968. (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 33375*	Version of cbv1h 1987 with a dv condition, which does not require ax-13 1968. (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 33376*	Version of cbv2h 1991 with a dv condition, which does not require ax-13 1968. (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 33377*	Version of cbv2 1992 with a dv condition, which does not require ax-13 1968. (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 33378*	Version of cbval 1994 with a dv condition, which does not require ax-13 1968. (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 33379*	Version of cbvex 1995 with a dv condition, which does not require ax-13 1968. (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 33380*	Version of cbvalv 1996 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	bj-cbvexvv 33381*	Version of cbvexv 1997 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
Theorem	bj-cbvaldv 33382*	Version of cbvald 1998 with a dv condition, which does not require ax-13 1968. (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 33383*	Version of cbvexd 1999 with a dv condition, which does not require ax-13 1968. (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 33384*	Version of cbval2 2000 with a dv condition, which does not require ax-13 1968. (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 33385*	Version of cbvex2 2001 with a dv condition, which does not require ax-13 1968. (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 33386*	Version of cbval2v 2003 with a dv condition, which does not require ax-13 1968. (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 33387*	Version of cbvex2v 2004 with a dv condition, which does not require ax-13 1968. (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 33388*	Version of cbvaldva 2005 with a dv condition, which does not require ax-13 1968. (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 33389*	Version of cbvexdva 2006 with a dv condition, which does not require ax-13 1968. (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 33390*	Version of cbvex4v 2007 with a dv condition, which does not require ax-13 1968. (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 33391*	Version of equs4 2008 with a dv condition, which does not require ax-13 1968 (neither ax-5 1680 nor ax-7 1739 nor ax-12 1803). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x ( x = y -> ph ) -> E. x ( x = y /\ ph ) )
Theorem	bj-equsalv 33392*	Version of equsal 2009 with a dv condition, which does not require ax-13 1968. (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 33393*	Version of equsalh 2010 with a dv condition, which does not require ax-13 1968. Remark: this is the same as equsalhw 1892. (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 33394*	Version of equsex 2011 with a dv condition, which does not require ax-13 1968. (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 33395*	Version of equsexh 2012 with a dv condition, which does not require ax-13 1968. Remark: the theorem axc9lem2 2013 has a dv version which is a simple consequence of ax5e 1682; the theorems nfeqf2 2014, dveeq2 2015, nfeqf1 2016, dveeq1 2017, nfeqf 2018, axc9 2019, ax13 2020, have dv versions which are simple consequences of ax-5 1680. (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 33396*	Version of axc11nlemOLD 2021 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x x = w -> A. y y = x )
Theorem	bj-axc11nv 33397*	Version of axc11n 2022 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> A. y y = x )
Theorem	bj-aecomsv 33398*	Version of aecoms 2025 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ph )   =>    |- ( A. y y = x -> ph )
Theorem	bj-naecomsv 33399*	Version of naecoms 2026 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ( -. A. x x = y -> ph )   =>    |- ( -. A. y y = x -> ph )
Theorem	bj-axc11v 33400*	Version of axc11 2027 with a dv condition, which does not require ax-13 1968. Remark: the following theorems (hbae 2028, nfae 2029, hbnae 2030, nfnae 2031, hbnaes 2032) would need to be totally unbundled to be proved without ax-13 1968, hence would be simple consequences of ax-5 1680 or nfv 1683. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ( A. x ph -> A. y ph ) )