P. 164 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16301-16400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bd3or 16301	A disjunction of three bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝜑    &   ⊢ BOUNDED 𝜓    &   ⊢ BOUNDED 𝜒    ⇒   ⊢ BOUNDED (𝜑 ∨ 𝜓 ∨ 𝜒)
Theorem	bd3an 16302	A conjunction of three bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝜑    &   ⊢ BOUNDED 𝜓    &   ⊢ BOUNDED 𝜒    ⇒   ⊢ BOUNDED (𝜑 ∧ 𝜓 ∧ 𝜒)
Theorem	bdth 16303	A truth (a (closed) theorem) is a bounded formula. (Contributed by BJ, 6-Oct-2019.)
⊢ 𝜑    ⇒   ⊢ BOUNDED 𝜑
Theorem	bdtru 16304	The truth value ⊤ is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED ⊤
Theorem	bdfal 16305	The truth value ⊥ is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED ⊥
Theorem	bdnth 16306	A falsity is a bounded formula. (Contributed by BJ, 6-Oct-2019.)
⊢ ¬ 𝜑    ⇒   ⊢ BOUNDED 𝜑
Theorem	bdnthALT 16307	Alternate proof of bdnth 16306 not using bdfal 16305. Then, bdfal 16305 can be proved from this theorem, using fal 1402. The total number of proof steps would be 17 (for bdnthALT 16307) + 3 = 20, which is more than 8 (for bdfal 16305) + 9 (for bdnth 16306) = 17. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝜑    ⇒   ⊢ BOUNDED 𝜑
Theorem	bdxor 16308	The exclusive disjunction of two bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝜑    &   ⊢ BOUNDED 𝜓    ⇒   ⊢ BOUNDED (𝜑 ⊻ 𝜓)
Theorem	bj-bdcel 16309*	Boundedness of a membership formula. (Contributed by BJ, 8-Dec-2019.)
⊢ BOUNDED 𝑦 = 𝐴    ⇒   ⊢ BOUNDED 𝐴 ∈ 𝑥
Theorem	bdab 16310	Membership in a class defined by class abstraction using a bounded formula, is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED 𝑥 ∈ {𝑦 ∣ 𝜑}
Theorem	bdcdeq 16311	Conditional equality of a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED CondEq(𝑥 = 𝑦 → 𝜑)
14.2.8.2  Bounded classes In line with our definitions of classes as extensions of predicates, it is useful to define a predicate for bounded classes, which is done in df-bdc 16313. Note that this notion is only a technical device which can be used to shorten proofs of (semantic) boundedness of formulas. As will be clear by the end of this subsection (see for instance bdop 16347), one can prove the boundedness of any concrete term using only setvars and bounded formulas, for instance, ⊢ BOUNDED 𝜑 ⇒ ⊢ BOUNDED ⟨{𝑥 ∣ 𝜑}, ({𝑦, suc 𝑧} × ⟨𝑡, ∅⟩)⟩. The proofs are long since one has to prove boundedness at each step of the construction, without being able to prove general theorems like ⊢ BOUNDED 𝐴 ⇒ ⊢ BOUNDED {𝐴}.
Syntax	wbdc 16312	Syntax for the predicate BOUNDED.
wff BOUNDED 𝐴
Definition	df-bdc 16313*	Define a bounded class as one such that membership in this class is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
⊢ (BOUNDED 𝐴 ↔ ∀𝑥BOUNDED 𝑥 ∈ 𝐴)
Theorem	bdceq 16314	Equality property for the predicate BOUNDED. (Contributed by BJ, 3-Oct-2019.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (BOUNDED 𝐴 ↔ BOUNDED 𝐵)
Theorem	bdceqi 16315	A class equal to a bounded one is bounded. Note the use of ax-ext 2211. See also bdceqir 16316. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    &   ⊢ 𝐴 = 𝐵    ⇒   ⊢ BOUNDED 𝐵
Theorem	bdceqir 16316	A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 16315) equality in the hypothesis, to work better with definitions (𝐵 is the definiendum that one wants to prove bounded; see comment of bd0r 16297). (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    &   ⊢ 𝐵 = 𝐴    ⇒   ⊢ BOUNDED 𝐵
Theorem	bdel 16317*	The belonging of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
⊢ (BOUNDED 𝐴 → BOUNDED 𝑥 ∈ 𝐴)
Theorem	bdeli 16318*	Inference associated with bdel 16317. Its converse is bdelir 16319. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    ⇒   ⊢ BOUNDED 𝑥 ∈ 𝐴
Theorem	bdelir 16319*	Inference associated with df-bdc 16313. Its converse is bdeli 16318. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝑥 ∈ 𝐴    ⇒   ⊢ BOUNDED 𝐴
Theorem	bdcv 16320	A setvar is a bounded class. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝑥
Theorem	bdcab 16321	A class defined by class abstraction using a bounded formula is bounded. (Contributed by BJ, 6-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED {𝑥 ∣ 𝜑}
Theorem	bdph 16322	A formula which defines (by class abstraction) a bounded class is bounded. (Contributed by BJ, 6-Oct-2019.)
⊢ BOUNDED {𝑥 ∣ 𝜑}    ⇒   ⊢ BOUNDED 𝜑
Theorem	bds 16323*	Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 16294; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 16294. (Contributed by BJ, 19-Nov-2019.)
⊢ BOUNDED 𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ BOUNDED 𝜓
Theorem	bdcrab 16324*	A class defined by restricted abstraction from a bounded class and a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    &   ⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED {𝑥 ∈ 𝐴 ∣ 𝜑}
Theorem	bdne 16325	Inequality of two setvars is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝑥 ≠ 𝑦
Theorem	bdnel 16326*	Non-membership of a setvar in a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝐴    ⇒   ⊢ BOUNDED 𝑥 ∉ 𝐴
Theorem	bdreu 16327*	Boundedness of existential uniqueness. Remark regarding restricted quantifiers: the formula ∀𝑥 ∈ 𝐴𝜑 need not be bounded even if 𝐴 and 𝜑 are. Indeed, V is bounded by bdcvv 16329, and ⊢ (∀𝑥 ∈ V𝜑 ↔ ∀𝑥𝜑) (in minimal propositional calculus), so by bd0 16296, if ∀𝑥 ∈ V𝜑 were bounded when 𝜑 is bounded, then ∀𝑥𝜑 would be bounded as well when 𝜑 is bounded, which is not the case. The same remark holds with ∃, ∃!, ∃*. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED ∃!𝑥 ∈ 𝑦 𝜑
Theorem	bdrmo 16328*	Boundedness of existential at-most-one. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED ∃*𝑥 ∈ 𝑦 𝜑
Theorem	bdcvv 16329	The universal class is bounded. The formulation may sound strange, but recall that here, "bounded" means "Δ0". (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED V
Theorem	bdsbc 16330	A formula resulting from proper substitution of a setvar for a setvar in a bounded formula is bounded. See also bdsbcALT 16331. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED [𝑦 / 𝑥]𝜑
Theorem	bdsbcALT 16331	Alternate proof of bdsbc 16330. (Contributed by BJ, 16-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED [𝑦 / 𝑥]𝜑
Theorem	bdccsb 16332	A class resulting from proper substitution of a setvar for a setvar in a bounded class is bounded. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝐴    ⇒   ⊢ BOUNDED ⦋𝑦 / 𝑥⦌𝐴
Theorem	bdcdif 16333	The difference of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    &   ⊢ BOUNDED 𝐵    ⇒   ⊢ BOUNDED (𝐴 ∖ 𝐵)
Theorem	bdcun 16334	The union of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    &   ⊢ BOUNDED 𝐵    ⇒   ⊢ BOUNDED (𝐴 ∪ 𝐵)
Theorem	bdcin 16335	The intersection of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    &   ⊢ BOUNDED 𝐵    ⇒   ⊢ BOUNDED (𝐴 ∩ 𝐵)
Theorem	bdss 16336	The inclusion of a setvar in a bounded class is a bounded formula. Note: apparently, we cannot prove from the present axioms that equality of two bounded classes is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    ⇒   ⊢ BOUNDED 𝑥 ⊆ 𝐴
Theorem	bdcnul 16337	The empty class is bounded. See also bdcnulALT 16338. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED ∅
Theorem	bdcnulALT 16338	Alternate proof of bdcnul 16337. Similarly, for the next few theorems proving boundedness of a class, one can either use their definition followed by bdceqir 16316, or use the corresponding characterizations of its elements followed by bdelir 16319. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ BOUNDED ∅
Theorem	bdeq0 16339	Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.)
⊢ BOUNDED 𝑥 = ∅
Theorem	bj-bd0el 16340	Boundedness of the formula "the empty set belongs to the setvar 𝑥". (Contributed by BJ, 30-Nov-2019.)
⊢ BOUNDED ∅ ∈ 𝑥
Theorem	bdcpw 16341	The power class of a bounded class is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    ⇒   ⊢ BOUNDED 𝒫 𝐴
Theorem	bdcsn 16342	The singleton of a setvar is bounded. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED {𝑥}
Theorem	bdcpr 16343	The pair of two setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED {𝑥, 𝑦}
Theorem	bdctp 16344	The unordered triple of three setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED {𝑥, 𝑦, 𝑧}
Theorem	bdsnss 16345*	Inclusion of a singleton of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝐴    ⇒   ⊢ BOUNDED {𝑥} ⊆ 𝐴
Theorem	bdvsn 16346*	Equality of a setvar with a singleton of a setvar is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝑥 = {𝑦}
Theorem	bdop 16347	The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.)
⊢ BOUNDED ⟨𝑥, 𝑦⟩
Theorem	bdcuni 16348	The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.)
⊢ BOUNDED ∪ 𝑥
Theorem	bdcint 16349	The intersection of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED ∩ 𝑥
Theorem	bdciun 16350*	The indexed union of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝐴    ⇒   ⊢ BOUNDED ∪ 𝑥 ∈ 𝑦 𝐴
Theorem	bdciin 16351*	The indexed intersection of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝐴    ⇒   ⊢ BOUNDED ∩ 𝑥 ∈ 𝑦 𝐴
Theorem	bdcsuc 16352	The successor of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED suc 𝑥
Theorem	bdeqsuc 16353*	Boundedness of the formula expressing that a setvar is equal to the successor of another. (Contributed by BJ, 21-Nov-2019.)
⊢ BOUNDED 𝑥 = suc 𝑦
Theorem	bj-bdsucel 16354	Boundedness of the formula "the successor of the setvar 𝑥 belongs to the setvar 𝑦". (Contributed by BJ, 30-Nov-2019.)
⊢ BOUNDED suc 𝑥 ∈ 𝑦
Theorem	bdcriota 16355*	A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.)
⊢ BOUNDED 𝜑    &   ⊢ ∃!𝑥 ∈ 𝑦 𝜑    ⇒   ⊢ BOUNDED (℩𝑥 ∈ 𝑦 𝜑)
14.2.9  CZF: Bounded separation In this section, we state the axiom scheme of bounded separation, which is part of CZF set theory.
Axiom	ax-bdsep 16356*	Axiom scheme of bounded (or restricted, or Δ0) separation. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. For the full axiom of separation, see ax-sep 4202. (Contributed by BJ, 5-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ ∀𝑎∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
Theorem	bdsep1 16357*	Version of ax-bdsep 16356 without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
Theorem	bdsep2 16358*	Version of ax-bdsep 16356 with one disjoint variable condition removed and without initial universal quantifier. Use bdsep1 16357 when sufficient. (Contributed by BJ, 5-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
Theorem	bdsepnft 16359*	Closed form of bdsepnf 16360. Version of ax-bdsep 16356 with one disjoint variable condition removed, the other disjoint variable condition replaced by a nonfreeness antecedent, and without initial universal quantifier. Use bdsep1 16357 when sufficient. (Contributed by BJ, 19-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ (∀𝑥Ⅎ𝑏𝜑 → ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)))
Theorem	bdsepnf 16360*	Version of ax-bdsep 16356 with one disjoint variable condition removed, the other disjoint variable condition replaced by a nonfreeness hypothesis, and without initial universal quantifier. See also bdsepnfALT 16361. Use bdsep1 16357 when sufficient. (Contributed by BJ, 5-Oct-2019.)
⊢ Ⅎ𝑏𝜑    &   ⊢ BOUNDED 𝜑    ⇒   ⊢ ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
Theorem	bdsepnfALT 16361*	Alternate proof of bdsepnf 16360, not using bdsepnft 16359. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑏𝜑    &   ⊢ BOUNDED 𝜑    ⇒   ⊢ ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
Theorem	bdzfauscl 16362*	Closed form of the version of zfauscl 4204 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
Theorem	bdbm1.3ii 16363*	Bounded version of bm1.3ii 4205. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝜑    &   ⊢ ∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥)    ⇒   ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)
Theorem	bj-axemptylem 16364*	Lemma for bj-axempty 16365 and bj-axempty2 16366. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4210 instead. (New usage is discouraged.)
⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 → ⊥)
Theorem	bj-axempty 16365*	Axiom of the empty set from bounded separation. It is provable from bounded separation since the intuitionistic FOL used in iset.mm assumes a nonempty universe. See axnul 4209. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4210 instead. (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ∈ 𝑥 ⊥
Theorem	bj-axempty2 16366*	Axiom of the empty set from bounded separation, alternate version to bj-axempty 16365. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4210 instead. (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	bj-nalset 16367*	nalset 4214 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥
Theorem	bj-vprc 16368	vprc 4216 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ ¬ V ∈ V
Theorem	bj-nvel 16369	nvel 4217 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ ¬ V ∈ 𝐴
Theorem	bj-vnex 16370	vnex 4215 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ ¬ ∃𝑥 𝑥 = V
Theorem	bdinex1 16371	Bounded version of inex1 4218. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐵    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∩ 𝐵) ∈ V
Theorem	bdinex2 16372	Bounded version of inex2 4219. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐵    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∩ 𝐴) ∈ V
Theorem	bdinex1g 16373	Bounded version of inex1g 4220. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐵    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)
Theorem	bdssex 16374	Bounded version of ssex 4221. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐴    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
Theorem	bdssexi 16375	Bounded version of ssexi 4222. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐴    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ 𝐴 ∈ V
Theorem	bdssexg 16376	Bounded version of ssexg 4223. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐴    ⇒   ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
Theorem	bdssexd 16377	Bounded version of ssexd 4224. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ BOUNDED 𝐴    ⇒   ⊢ (𝜑 → 𝐴 ∈ V)
Theorem	bdrabexg 16378*	Bounded version of rabexg 4228. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝜑    &   ⊢ BOUNDED 𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	bj-inex 16379	The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∩ 𝐵) ∈ V)
Theorem	bj-intexr 16380	intexr 4235 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
Theorem	bj-intnexr 16381	intnexr 4236 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ (∩ 𝐴 = V → ¬ ∩ 𝐴 ∈ V)
Theorem	bj-zfpair2 16382	Proof of zfpair2 4295 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
⊢ {𝑥, 𝑦} ∈ V
Theorem	bj-prexg 16383	Proof of prexg 4296 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
Theorem	bj-snexg 16384	snexg 4269 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
Theorem	bj-snex 16385	snex 4270 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ∈ V
Theorem	bj-sels 16386*	If a class is a set, then it is a member of a set. (Copied from set.mm.) (Contributed by BJ, 3-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝐴 ∈ 𝑥)
Theorem	bj-axun2 16387*	axun2 4527 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))
Theorem	bj-uniex2 16388*	uniex2 4528 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
⊢ ∃𝑦 𝑦 = ∪ 𝑥
Theorem	bj-uniex 16389	uniex 4529 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∪ 𝐴 ∈ V
Theorem	bj-uniexg 16390	uniexg 4531 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
Theorem	bj-unex 16391	unex 4533 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∪ 𝐵) ∈ V
Theorem	bdunexb 16392	Bounded version of unexb 4534. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐴    &   ⊢ BOUNDED 𝐵    ⇒   ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V)
Theorem	bj-unexg 16393	unexg 4535 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
Theorem	bj-sucexg 16394	sucexg 4591 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ∈ V)
Theorem	bj-sucex 16395	sucex 4592 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ suc 𝐴 ∈ V
14.2.9.1  Delta_0-classical logic
Axiom	ax-bj-d0cl 16396	Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.)
⊢ BOUNDED 𝜑    ⇒   ⊢ DECID 𝜑
Theorem	bj-d0clsepcl 16397	Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.)
⊢ DECID 𝜑
14.2.9.2  Inductive classes and the class of natural number ordinals
Syntax	wind 16398	Syntax for inductive classes.
wff Ind 𝐴
Definition	df-bj-ind 16399*	Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.)
⊢ (Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
Theorem	bj-indsuc 16400	A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.)
⊢ (Ind 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴))