P. 167 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16601-16700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bdth 16601	A truth (a (closed) theorem) is a bounded formula. (Contributed by BJ, 6-Oct-2019.)
⊢ 𝜑    ⇒   ⊢ BOUNDED 𝜑
Theorem	bdtru 16602	The truth value ⊤ is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED ⊤
Theorem	bdfal 16603	The truth value ⊥ is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED ⊥
Theorem	bdnth 16604	A falsity is a bounded formula. (Contributed by BJ, 6-Oct-2019.)
⊢ ¬ 𝜑    ⇒   ⊢ BOUNDED 𝜑
Theorem	bdnthALT 16605	Alternate proof of bdnth 16604 not using bdfal 16603. Then, bdfal 16603 can be proved from this theorem, using fal 1405. The total number of proof steps would be 17 (for bdnthALT 16605) + 3 = 20, which is more than 8 (for bdfal 16603) + 9 (for bdnth 16604) = 17. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝜑    ⇒   ⊢ BOUNDED 𝜑
Theorem	bdxor 16606	The exclusive disjunction of two bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝜑    &   ⊢ BOUNDED 𝜓    ⇒   ⊢ BOUNDED (𝜑 ⊻ 𝜓)
Theorem	bj-bdcel 16607*	Boundedness of a membership formula. (Contributed by BJ, 8-Dec-2019.)
⊢ BOUNDED 𝑦 = 𝐴    ⇒   ⊢ BOUNDED 𝐴 ∈ 𝑥
Theorem	bdab 16608	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 16609	Conditional equality of a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED CondEq(𝑥 = 𝑦 → 𝜑)
14.3.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 16611. 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 16645), 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 16610	Syntax for the predicate BOUNDED.
wff BOUNDED 𝐴
Definition	df-bdc 16611*	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 16612	Equality property for the predicate BOUNDED. (Contributed by BJ, 3-Oct-2019.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (BOUNDED 𝐴 ↔ BOUNDED 𝐵)
Theorem	bdceqi 16613	A class equal to a bounded one is bounded. Note the use of ax-ext 2214. See also bdceqir 16614. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    &   ⊢ 𝐴 = 𝐵    ⇒   ⊢ BOUNDED 𝐵
Theorem	bdceqir 16614	A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 16613) equality in the hypothesis, to work better with definitions (𝐵 is the definiendum that one wants to prove bounded; see comment of bd0r 16595). (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    &   ⊢ 𝐵 = 𝐴    ⇒   ⊢ BOUNDED 𝐵
Theorem	bdel 16615*	The belonging of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
⊢ (BOUNDED 𝐴 → BOUNDED 𝑥 ∈ 𝐴)
Theorem	bdeli 16616*	Inference associated with bdel 16615. Its converse is bdelir 16617. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    ⇒   ⊢ BOUNDED 𝑥 ∈ 𝐴
Theorem	bdelir 16617*	Inference associated with df-bdc 16611. Its converse is bdeli 16616. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝑥 ∈ 𝐴    ⇒   ⊢ BOUNDED 𝐴
Theorem	bdcv 16618	A setvar is a bounded class. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝑥
Theorem	bdcab 16619	A class defined by class abstraction using a bounded formula is bounded. (Contributed by BJ, 6-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED {𝑥 ∣ 𝜑}
Theorem	bdph 16620	A formula which defines (by class abstraction) a bounded class is bounded. (Contributed by BJ, 6-Oct-2019.)
⊢ BOUNDED {𝑥 ∣ 𝜑}    ⇒   ⊢ BOUNDED 𝜑
Theorem	bds 16621*	Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 16592; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 16592. (Contributed by BJ, 19-Nov-2019.)
⊢ BOUNDED 𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ BOUNDED 𝜓
Theorem	bdcrab 16622*	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 16623	Inequality of two setvars is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝑥 ≠ 𝑦
Theorem	bdnel 16624*	Non-membership of a setvar in a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝐴    ⇒   ⊢ BOUNDED 𝑥 ∉ 𝐴
Theorem	bdreu 16625*	Boundedness of existential uniqueness. Remark regarding restricted quantifiers: the formula ∀𝑥 ∈ 𝐴𝜑 need not be bounded even if 𝐴 and 𝜑 are. Indeed, V is bounded by bdcvv 16627, and ⊢ (∀𝑥 ∈ V𝜑 ↔ ∀𝑥𝜑) (in minimal propositional calculus), so by bd0 16594, 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 16626*	Boundedness of existential at-most-one. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED ∃*𝑥 ∈ 𝑦 𝜑
Theorem	bdcvv 16627	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 16628	A formula resulting from proper substitution of a setvar for a setvar in a bounded formula is bounded. See also bdsbcALT 16629. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED [𝑦 / 𝑥]𝜑
Theorem	bdsbcALT 16629	Alternate proof of bdsbc 16628. (Contributed by BJ, 16-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ BOUNDED 𝜑    ⇒   ⊢ BOUNDED [𝑦 / 𝑥]𝜑
Theorem	bdccsb 16630	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 16631	The difference of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    &   ⊢ BOUNDED 𝐵    ⇒   ⊢ BOUNDED (𝐴 ∖ 𝐵)
Theorem	bdcun 16632	The union of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    &   ⊢ BOUNDED 𝐵    ⇒   ⊢ BOUNDED (𝐴 ∪ 𝐵)
Theorem	bdcin 16633	The intersection of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    &   ⊢ BOUNDED 𝐵    ⇒   ⊢ BOUNDED (𝐴 ∩ 𝐵)
Theorem	bdss 16634	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 16635	The empty class is bounded. See also bdcnulALT 16636. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED ∅
Theorem	bdcnulALT 16636	Alternate proof of bdcnul 16635. Similarly, for the next few theorems proving boundedness of a class, one can either use their definition followed by bdceqir 16614, or use the corresponding characterizations of its elements followed by bdelir 16617. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ BOUNDED ∅
Theorem	bdeq0 16637	Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.)
⊢ BOUNDED 𝑥 = ∅
Theorem	bj-bd0el 16638	Boundedness of the formula "the empty set belongs to the setvar 𝑥". (Contributed by BJ, 30-Nov-2019.)
⊢ BOUNDED ∅ ∈ 𝑥
Theorem	bdcpw 16639	The power class of a bounded class is bounded. (Contributed by BJ, 3-Oct-2019.)
⊢ BOUNDED 𝐴    ⇒   ⊢ BOUNDED 𝒫 𝐴
Theorem	bdcsn 16640	The singleton of a setvar is bounded. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED {𝑥}
Theorem	bdcpr 16641	The pair of two setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED {𝑥, 𝑦}
Theorem	bdctp 16642	The unordered triple of three setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED {𝑥, 𝑦, 𝑧}
Theorem	bdsnss 16643*	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 16644*	Equality of a setvar with a singleton of a setvar is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED 𝑥 = {𝑦}
Theorem	bdop 16645	The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.)
⊢ BOUNDED ⟨𝑥, 𝑦⟩
Theorem	bdcuni 16646	The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.)
⊢ BOUNDED ∪ 𝑥
Theorem	bdcint 16647	The intersection of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED ∩ 𝑥
Theorem	bdciun 16648*	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 16649*	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 16650	The successor of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
⊢ BOUNDED suc 𝑥
Theorem	bdeqsuc 16651*	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 16652	Boundedness of the formula "the successor of the setvar 𝑥 belongs to the setvar 𝑦". (Contributed by BJ, 30-Nov-2019.)
⊢ BOUNDED suc 𝑥 ∈ 𝑦
Theorem	bdcriota 16653*	A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.)
⊢ BOUNDED 𝜑    &   ⊢ ∃!𝑥 ∈ 𝑦 𝜑    ⇒   ⊢ BOUNDED (℩𝑥 ∈ 𝑦 𝜑)
14.3.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 16654*	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 4228. (Contributed by BJ, 5-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ ∀𝑎∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
Theorem	bdsep1 16655*	Version of ax-bdsep 16654 without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
Theorem	bdsep2 16656*	Version of ax-bdsep 16654 with one disjoint variable condition removed and without initial universal quantifier. Use bdsep1 16655 when sufficient. (Contributed by BJ, 5-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
Theorem	bdsepnft 16657*	Closed form of bdsepnf 16658. Version of ax-bdsep 16654 with one disjoint variable condition removed, the other disjoint variable condition replaced by a nonfreeness antecedent, and without initial universal quantifier. Use bdsep1 16655 when sufficient. (Contributed by BJ, 19-Oct-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ (∀𝑥Ⅎ𝑏𝜑 → ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑)))
Theorem	bdsepnf 16658*	Version of ax-bdsep 16654 with one disjoint variable condition removed, the other disjoint variable condition replaced by a nonfreeness hypothesis, and without initial universal quantifier. See also bdsepnfALT 16659. Use bdsep1 16655 when sufficient. (Contributed by BJ, 5-Oct-2019.)
⊢ Ⅎ𝑏𝜑    &   ⊢ BOUNDED 𝜑    ⇒   ⊢ ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
Theorem	bdsepnfALT 16659*	Alternate proof of bdsepnf 16658, not using bdsepnft 16657. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑏𝜑    &   ⊢ BOUNDED 𝜑    ⇒   ⊢ ∃𝑏∀𝑥(𝑥 ∈ 𝑏 ↔ (𝑥 ∈ 𝑎 ∧ 𝜑))
Theorem	bdzfauscl 16660*	Closed form of the version of zfauscl 4230 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.)
⊢ BOUNDED 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)))
Theorem	bdbm1.3ii 16661*	Bounded version of bm1.3ii 4231. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝜑    &   ⊢ ∃𝑥∀𝑦(𝜑 → 𝑦 ∈ 𝑥)    ⇒   ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝜑)
Theorem	bj-axemptylem 16662*	Lemma for bj-axempty 16663 and bj-axempty2 16664. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4236 instead. (New usage is discouraged.)
⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 → ⊥)
Theorem	bj-axempty 16663*	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 4235. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4236 instead. (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ∈ 𝑥 ⊥
Theorem	bj-axempty2 16664*	Axiom of the empty set from bounded separation, alternate version to bj-axempty 16663. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4236 instead. (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	bj-nalset 16665*	nalset 4240 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ ¬ ∃𝑥∀𝑦 𝑦 ∈ 𝑥
Theorem	bj-vprc 16666	vprc 4242 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ ¬ V ∈ V
Theorem	bj-nvel 16667	nvel 4243 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ ¬ V ∈ 𝐴
Theorem	bj-vnex 16668	vnex 4241 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ ¬ ∃𝑥 𝑥 = V
Theorem	bdinex1 16669	Bounded version of inex1 4244. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐵    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∩ 𝐵) ∈ V
Theorem	bdinex2 16670	Bounded version of inex2 4245. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐵    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∩ 𝐴) ∈ V
Theorem	bdinex1g 16671	Bounded version of inex1g 4246. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐵    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)
Theorem	bdssex 16672	Bounded version of ssex 4247. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐴    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)
Theorem	bdssexi 16673	Bounded version of ssexi 4248. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐴    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ 𝐴 ∈ V
Theorem	bdssexg 16674	Bounded version of ssexg 4249. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐴    ⇒   ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
Theorem	bdssexd 16675	Bounded version of ssexd 4250. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ BOUNDED 𝐴    ⇒   ⊢ (𝜑 → 𝐴 ∈ V)
Theorem	bdrabexg 16676*	Bounded version of rabexg 4255. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝜑    &   ⊢ BOUNDED 𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	bj-inex 16677	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 16678	intexr 4262 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ (∩ 𝐴 ∈ V → 𝐴 ≠ ∅)
Theorem	bj-intnexr 16679	intnexr 4263 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ (∩ 𝐴 = V → ¬ ∩ 𝐴 ∈ V)
Theorem	bj-zfpair2 16680	Proof of zfpair2 4323 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
⊢ {𝑥, 𝑦} ∈ V
Theorem	bj-prexg 16681	Proof of prexg 4325 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V)
Theorem	bj-snexg 16682	snexg 4297 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V)
Theorem	bj-snex 16683	snex 4298 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ∈ V
Theorem	bj-sels 16684*	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 16685*	axun2 4556 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))
Theorem	bj-uniex2 16686*	uniex2 4557 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
⊢ ∃𝑦 𝑦 = ∪ 𝑥
Theorem	bj-uniex 16687	uniex 4558 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∪ 𝐴 ∈ V
Theorem	bj-uniexg 16688	uniexg 4560 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
Theorem	bj-unex 16689	unex 4562 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∪ 𝐵) ∈ V
Theorem	bdunexb 16690	Bounded version of unexb 4563. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED 𝐴    &   ⊢ BOUNDED 𝐵    ⇒   ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V)
Theorem	bj-unexg 16691	unexg 4564 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
Theorem	bj-sucexg 16692	sucexg 4620 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ∈ V)
Theorem	bj-sucex 16693	sucex 4621 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ suc 𝐴 ∈ V
14.3.9.1  Delta_0-classical logic
Axiom	ax-bj-d0cl 16694	Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.) New usage is discouraged since this statement is not intuitionnistic. (New usage is discouraged.)
⊢ BOUNDED 𝜑    ⇒   ⊢ DECID 𝜑
Theorem	bj-d0clsepcl 16695	Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.) New usage is discouraged since this statement is not intuitionnistic. (New usage is discouraged.)
⊢ DECID 𝜑
14.3.9.2  Inductive classes and the class of natural number ordinals
Syntax	wind 16696	Syntax for inductive classes.
wff Ind 𝐴
Definition	df-bj-ind 16697*	Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.)
⊢ (Ind 𝐴 ↔ (∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴))
Theorem	bj-indsuc 16698	A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.)
⊢ (Ind 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴))
Theorem	bj-indeq 16699	Equality property for Ind. (Contributed by BJ, 30-Nov-2019.)
⊢ (𝐴 = 𝐵 → (Ind 𝐴 ↔ Ind 𝐵))
Theorem	bj-bdind 16700	Boundedness of the formula "the setvar 𝑥 is an inductive class". (Contributed by BJ, 30-Nov-2019.)
⊢ BOUNDED Ind 𝑥