P. 328 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32701-32800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-hbext 32701	Closed form of hbex 2156. (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 32702	Closed form of nfal 2153. (Contributed by BJ, 2-May-2019.)
|- ( A. x F/ y ph -> F/ y A. x ph )
Theorem	bj-nfext 32703	Closed form of nfex 2154. (Contributed by BJ, 10-Oct-2019.)
|- ( A. x F/ y ph -> F/ y E. x ph )
Theorem	bj-eeanvw 32704*	Version of eeanv 2182 with a DV condition on x , y not requiring ax-11 2034. (The same can be done with eeeanv 2183 and ee4anv 2184.) (Contributed by BJ, 29-Sep-2019.) (Proof modification is discouraged.)
|- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )
Theorem	bj-modal4e 32705	Dual statement of hba1 2151 (which is modal-4 ). (Contributed by BJ, 21-Dec-2020.)
|- ( E. x E. x ph -> E. x ph )
Theorem	bj-modalb 32706	A short form of the axiom B of modal logic. (Contributed by BJ, 4-Apr-2021.)
|- ( -. ph -> A. x -. A. x ph )
20.14.4.10  Adding ax-13
Theorem	bj-axc10 32707	Alternate (shorter) proof of axc10 2252. One can prove a version with DV(x,y) without ax-13 2246, by using ax6ev 1890 instead of ax6e 2250. (Contributed by BJ, 31-Mar-2021.) (Proof modification is discouraged.)
|- ( A. x ( x = y -> A. x ph ) -> ph )
Theorem	bj-alequex 32708	A fol lemma. See bj-alequexv 32655 for a version with a DV condition requiring fewer axioms. Can be used to reduce the proof of spimt 2253 from 133 to 112 bytes. (Contributed by BJ, 6-Oct-2018.)
|- ( A. x ( x = y -> ph ) -> E. x ph )
Theorem	bj-spimt2 32709	A step in the proof of spimt 2253. (Contributed by BJ, 2-May-2019.)
|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( ( E. x ps -> ps ) -> ( A. x ph -> ps ) ) )
Theorem	bj-cbv3ta 32710	Closed form of cbv3 2265. (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 32711	Closed form of cbv3 2265. (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 32712	A theorem close to a closed form of hbsb3 2364. (Contributed by BJ, 2-May-2019.)
|- ( A. x ( ph -> A. y ph ) -> ( [ y / x ] ph -> A. x [ y / x ] ph ) )
Theorem	bj-hbsb3 32713	Shorter proof of hbsb3 2364. (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.)
|- ( ph -> A. y ph )   =>    |- ( [ y / x ] ph -> A. x [ y / x ] ph )
Theorem	bj-nfs1t 32714	A theorem close to a closed form of nfs1 2365. (Contributed by BJ, 2-May-2019.)
|- ( A. x ( ph -> A. y ph ) -> F/ x [ y / x ] ph )
Theorem	bj-nfs1t2 32715	A theorem close to a closed form of nfs1 2365. (Contributed by BJ, 2-May-2019.)
|- ( A. x F/ y ph -> F/ x [ y / x ] ph )
Theorem	bj-nfs1 32716	Shorter proof of nfs1 2365 (three essential steps instead of four). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.)
|- F/ y ph   =>    |- F/ x [ y / x ] ph
20.14.4.11  Removing dependencies on ax-13 (and ax-11) It is known that ax-13 2246 is logically redundant (see ax13w 2013 and the head comment of the section "Logical redundancy of ax-10--13"). More precisely, one can remove dependency on ax-13 2246 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 2246 with ax13w 2013. This section is an experiment to see in practice if (partially) unbundled versions of existing theorems can be proved more efficiently without ax-13 2246 (and using ax6v 1889 / ax6ev 1890 instead of ax-6 1888 / ax6e 2250, as is currently done). One reason to be optimistic is that the first few utility theorems using ax-13 2246 (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 2246, labeled bj-xxxv (we follow the proof of xxx but use ax6v 1889 and ax6ev 1890 instead of ax-6 1888 and ax6e 2250, and ax-5 1839 instead of ax13v 2247; 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 2246, so as to remove dependencies on ax-13 2246 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 2034, typically by replacing a non-free hypothesis with a dv condition (see bj-cbv3v2 32727 and following theorems).
Theorem	bj-axc10v 32717*	Version of axc10 2252 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x ( x = y -> A. x ph ) -> ph )
Theorem	bj-spimtv 32718*	Version of spimt 2253 with a dv condition, which does not require ax-13 2246. (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-spimedv 32719*	Version of spimed 2255 with a dv condition, which does not require ax-13 2246. (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 32720*	Version of spime 2256 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ x ph   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( ph -> E. x ps )
Theorem	bj-spimvv 32721*	Version of spimv 2257 and spimv1 2115 with a dv condition, which does not require ax-13 2246. UPDATE: this is spimvw 1927. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	bj-spimevv 32722*	Version of spimev 2259 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph -> ps ) )   =>    |- ( ph -> E. x ps )
Theorem	bj-spvv 32723*	Version of spv 2260 with a dv condition, which does not require ax-7 1935, ax-12 2047, ax-13 2246. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	bj-speiv 32724*	Version of spei 2261 with a dv condition, which does not require ax-13 2246 (neither ax-7 1935 nor ax-12 2047). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ps   =>    |- E. x ph
Theorem	bj-chvarv 32725*	Version of chvar 2262 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	bj-chvarvv 32726*	Version of chvarv 2263 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	bj-cbv3v2 32727*	Version of cbv3 2265 with two dv conditions, which does not require ax-11 2034 nor ax-13 2246. (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-cbv3hv2 32728*	Version of cbv3h 2266 with two dv conditions, which does not require ax-11 2034 nor ax-13 2246. (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 32729*	Version of cbv1 2267 with a dv condition, which does not require ax-13 2246. (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 32730*	Version of cbv1h 2268 with a dv condition, which does not require ax-13 2246. (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 32731*	Version of cbv2h 2269 with a dv condition, which does not require ax-13 2246. (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 32732*	Version of cbv2 2270 with a dv condition, which does not require ax-13 2246. (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-cbvalvv 32733*	Version of cbvalv 2273 with a dv condition, which does not require ax-13 2246. UPDATE: this is cbvalvw 1969 (which is proved with fewer axioms). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	bj-cbvexvv 32734*	Version of cbvexv 2275 with a dv condition, which does not require ax-13 2246. UPDATE: this is cbvexvw 1970 (which is proved with fewer axioms). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
Theorem	bj-cbvaldv 32735*	Version of cbvald 2277 with a dv condition, which does not require ax-13 2246. (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 32736*	Version of cbvexd 2278 with a dv condition, which does not require ax-13 2246. (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 32737*	Version of cbval2 2279 with a dv condition, which does not require ax-13 2246. (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 32738*	Version of cbvex2 2280 with a dv condition, which does not require ax-13 2246. (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 32739*	Version of cbval2v 2285 with a dv condition, which does not require ax-13 2246. (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 32740*	Version of cbvex2v 2287 with a dv condition, which does not require ax-13 2246. (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 32741*	Version of cbvaldva 2281 with a dv condition, which does not require ax-13 2246. (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 32742*	Version of cbvexdva 2283 with a dv condition, which does not require ax-13 2246. (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 32743*	Version of cbvex4v 2289 with a dv condition, which does not require ax-13 2246. (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-equsalhv 32744*	Version of equsalh 2294 with a dv condition, which does not require ax-13 2246. Remark: this is the same as equsalhw 2123. Remarks: equsexvw 1932 has been moved to Main; the theorem ax13lem2 2296 has a dv version which is a simple consequence of ax5e 1841; the theorems nfeqf2 2297, dveeq2 2298, nfeqf1 2299, dveeq1 2300, nfeqf 2301, axc9 2302, ax13 2249, have dv versions which are simple consequences of ax-5 1839. (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-axc11nv 32745*	Version of axc11n 2307 with a dv condition; instance of aevlem 1981. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> A. y y = x )
Theorem	bj-aecomsv 32746*	Version of aecoms 2312 with a dv condition, provable from Tarski's FOL. The corresponding version of naecoms 2313 should not be very useful since -. A. x x = y, DV(x, y) is true when the universe has at least two objects (see bj-dtru 32797). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ph )   =>    |- ( A. y y = x -> ph )
Theorem	bj-axc11v 32747*	Version of axc11 2314 with a dv condition, which does not require ax-13 2246 nor ax-10 2019. Remark: the following theorems (hbae 2315, nfae 2316, hbnae 2317, nfnae 2318, hbnaes 2319) would need to be totally unbundled to be proved without ax-13 2246, hence would be simple consequences of ax-5 1839 or nfv 1843. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
Theorem	bj-dral1v 32748*	Version of dral1 2325 with a dv condition, which does not require ax-13 2246. Remark: the corresponding versions for dral2 2324 and drex2 2328 are instances of albidv 1849 and exbidv 1850 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 32749*	Version of drex1 2327 with a dv condition, which does not require ax-13 2246. (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 32750*	Version of drnf1 2329 with a dv condition, which does not require ax-13 2246. (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 32751*	Version of drnf2 2330 with a dv condition, which does not require ax-13 2246. Could be labeled "nfbidv". Note that the version of axc15 2303 with a dv condition is actually ax12v2 2049 (up to adding a superfluous antecedent). (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-equs45fv 32752*	Version of equs45f 2350 with a dv condition, which does not require ax-13 2246. Note that the version of equs5 2351 with a dv condition is actually sb56 2150 (up to adding a superfluous antecedent). (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-sb2v 32753*	Version of sb2 2352 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x ( x = y -> ph ) -> [ y / x ] ph )
Theorem	bj-stdpc4v 32754*	Version of stdpc4 2353 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( A. x ph -> [ y / x ] ph )
Theorem	bj-2stdpc4v 32755*	Version of 2stdpc4 2354 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x A. y ph -> [ z / x ] [ w / y ] ph )
Theorem	bj-sb3v 32756*	Version of sb3 2355 with a dv condition, which does not require ax-13 2246. This allows to remove ax-13 2246 from sb5 2430 (see bj-sb5 32768). (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( E. x ( x = y /\ ph ) -> [ y / x ] ph )
Theorem	bj-sb4v 32757*	Version of sb4 2356 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 23-Jun-2019.) Together with bj-sb2v 32753, this allosw to remove ax-13 2246 from sb6 2429 (see bj-sb6 32767). Note that this subsumes the version of sb4b 2358 with a dv condition. (Proof modification is discouraged.)
|- ( [ y / x ] ph -> A. x ( x = y -> ph ) )
Theorem	bj-hbs1 32758*	Version of hbsb2 2359 with a dv condition, which does not require ax-13 2246, and removal of ax-13 2246 from hbs1 2436. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( [ y / x ] ph -> A. x [ y / x ] ph )
Theorem	bj-nfs1v 32759*	Version of nfsb2 2360 with a dv condition, which does not require ax-13 2246, and removal of ax-13 2246 from nfs1v 2437. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- F/ x [ y / x ] ph
Theorem	bj-hbsb2av 32760*	Version of hbsb2a 2361 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
|- ( [ y / x ] A. y ph -> A. x [ y / x ] ph )
Theorem	bj-hbsb3v 32761*	Version of hbsb3 2364 with a dv condition, which does not require ax-13 2246. (Remark: the unbundled version of nfs1 2365 is given by bj-nfs1v 32759.) (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 32762*	Version of equsb1 2368 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
|- [ y / x ] x = y
Theorem	bj-sbftv 32763*	Version of sbft 2379 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ( F/ x ph -> ( [ y / x ] ph <-> ph ) )
Theorem	bj-sbfv 32764*	Version of sbf 2380 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ x ph   =>    |- ( [ y / x ] ph <-> ph )
Theorem	bj-sbfvv 32765*	Version of sbf 2380 with two dv conditions, which does not require ax-10 2019 nor ax-13 2246. (Contributed by BJ, 1-May-2021.) (Proof modification is discouraged.)
|- ( [ y / x ] ph <-> ph )
Theorem	bj-sbtv 32766*	Version of sbt 2419 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- ph   =>    |- [ y / x ] ph
Theorem	bj-sb6 32767*	Remove dependency on ax-13 2246 from sb6 2429. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
|- ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
Theorem	bj-sb5 32768*	Remove dependency on ax-13 2246 from sb5 2430. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
|- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )
Theorem	bj-axext3 32769*	Remove dependency on ax-13 2246 from axext3 2604. (Contributed by BJ, 12-Jul-2019.) (Proof modification is discouraged.)
|- ( A. z ( z e. x <-> z e. y ) -> x = y )
Theorem	bj-axext4 32770*	Remove dependency on ax-13 2246 from axext4 2606. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- ( x = y <-> A. z ( z e. x <-> z e. y ) )
Theorem	bj-hbab1 32771*	Remove dependency on ax-13 2246 from hbab1 2611. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( y e. { x | ph } -> A. x y e. { x | ph } )
Theorem	bj-nfsab1 32772*	Remove dependency on ax-13 2246 from nfsab1 2612. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- F/ x y e. { x | ph }
Theorem	bj-abeq2 32773*	Remove dependency on ax-13 2246 from abeq2 2732. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) )
Theorem	bj-abeq1 32774*	Remove dependency on ax-13 2246 from abeq1 2733. Remark: the theorems abeq2i 2735, abeq1i 2736, abeq2d 2734 do not use ax-11 2034 or ax-13 2246. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( { x | ph } = A <-> A. x ( ph <-> x e. A ) )
Theorem	bj-abbi 32775	Remove dependency on ax-13 2246 from abbi 2737. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
Theorem	bj-abbi2i 32776*	Remove dependency on ax-13 2246 from abbi2i 2738. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( x e. A <-> ph )   =>    |- A = { x | ph }
Theorem	bj-abbii 32777	Remove dependency on ax-13 2246 from abbii 2739. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( ph <-> ps )   =>    |- { x | ph } = { x | ps }
Theorem	bj-abbid 32778	Remove dependency on ax-13 2246 from abbid 2740. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x | ps } = { x | ch } )
Theorem	bj-abbidv 32779*	Remove dependency on ax-13 2246 from abbidv 2741. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x | ps } = { x | ch } )
Theorem	bj-abbi2dv 32780*	Remove dependency on ax-13 2246 from abbi2dv 2742. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( ph -> ( x e. A <-> ps ) )   =>    |- ( ph -> A = { x | ps } )
Theorem	bj-abbi1dv 32781*	Remove dependency on ax-13 2246 from abbi1dv 2743. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( ph -> ( ps <-> x e. A ) )   =>    |- ( ph -> { x | ps } = A )
Theorem	bj-abid2 32782*	Remove dependency on ax-13 2246 from abid2 2745. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- { x | x e. A } = A
Theorem	bj-clabel 32783*	Remove dependency on ax-13 2246 from clabel 2749 (note the absence of DV conditions among variables in the LHS). (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( { x | ph } e. A <-> E. y ( y e. A /\ A. x ( x e. y <-> ph ) ) )
Theorem	bj-sbab 32784*	Remove dependency on ax-13 2246 from sbab 2750 (note the absence of DV conditions among variables in the LHS). (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
|- ( x = y -> A = { z | [ y / x ] z e. A } )
Theorem	bj-nfab1 32785	Remove dependency on ax-13 2246 from nfab1 2766 (note the absence of DV conditions). (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- F/_ x { x | ph }
Theorem	bj-vjust 32786	Remove dependency on ax-13 2246 from vjust 3201 (note the absence of DV conditions). Soundness justification theorem for df-v 3202. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- { x | x = x } = { y | y = y }
Theorem	bj-cdeqab 32787*	Remove dependency on ax-13 2246 from cdeqab 3425. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- CondEq ( x = y -> ( ph <-> ps ) )   =>    |- CondEq ( x = y -> { z | ph } = { z | ps } )
Theorem	bj-axrep1 32788*	Remove dependency on ax-13 2246 from axrep1 4772. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ ph ) ) )
Theorem	bj-axrep2 32789*	Remove dependency on ax-13 2246 from axrep2 4773. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) )
Theorem	bj-axrep3 32790*	Remove dependency on ax-13 2246 from axrep3 4774. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. w /\ A. y ph ) ) )
Theorem	bj-axrep4 32791*	Remove dependency on ax-13 2246 from axrep4 4775. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ z ph   =>    |- ( A. x E. z A. y ( ph -> y = z ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )
Theorem	bj-axrep5 32792*	Remove dependency on ax-13 2246 from axrep5 4776. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- F/ z ph   =>    |- ( A. x ( x e. w -> E. z A. y ( ph -> y = z ) ) -> E. z A. y ( y e. z <-> E. x ( x e. w /\ ph ) ) )
Theorem	bj-axsep 32793*	Remove dependency on ax-13 2246 from axsep 4780. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
Theorem	bj-nalset 32794*	Remove dependency on ax-13 2246 from nalset 4795. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- -. E. x A. y y e. x
Theorem	bj-zfpow 32795*	Remove dependency on ax-13 2246 from zfpow 4844. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- E. x A. y ( A. x ( x e. y -> x e. z ) -> y e. x )
Theorem	bj-el 32796*	Remove dependency on ax-13 2246 from el 4847. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- E. y x e. y
Theorem	bj-dtru 32797*	Remove dependency on ax-13 2246 from dtru 4857. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
|- -. A. x x = y
Theorem	bj-axc16b 32798*	Remove dependency on ax-13 2246 from axc16b 4858. (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
|- ( A. x x = y -> ( ph -> A. x ph ) )
Theorem	bj-eunex 32799	Remove dependency on ax-13 2246 from eunex 4859. (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
|- ( E! x ph -> E. x -. ph )
Theorem	bj-dtrucor 32800*	Remove dependency on ax-13 2246 from dtrucor 4900. (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
|- x = y   =>    |- x =/= y