P. 127 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12601-12700   *Has distinct variable group(s)

Type	Label	Description
Statement
Axiom	ax-bdsb 12601	A formula resulting from proper substitution in a bounded formula is bounded. This probably cannot be proved from the other axioms, since neither the definiens in df-sb 1704, nor probably any other equivalent formula, is syntactically bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED [ y / x ] ph
Theorem	bdeq 12602	Equality property for the predicate BOUNDED. (Contributed by BJ, 3-Oct-2019.)
|- ( ph <-> ps )   =>    |- (BOUNDED ph <-> BOUNDED ps )
Theorem	bd0 12603	A formula equivalent to a bounded one is bounded. See also bd0r 12604. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   &    |- ( ph <-> ps )   =>    |- BOUNDED ps
Theorem	bd0r 12604	A formula equivalent to a bounded one is bounded. Stated with a commuted (compared with bd0 12603) biconditional in the hypothesis, to work better with definitions ( ps is the definiendum that one wants to prove bounded). (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   &    |- ( ps <-> ph )   =>    |- BOUNDED ps
Theorem	bdbi 12605	A biconditional between two bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph <-> ps )
Theorem	bdstab 12606	Stability of a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED STAB ph
Theorem	bddc 12607	Decidability of a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED DECID ph
Theorem	bd3or 12608	A disjunction of three bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   &    |- BOUNDED ps   &    |- BOUNDED ch   =>    |- BOUNDED ( ph \/ ps \/ ch )
Theorem	bd3an 12609	A conjunction of three bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   &    |- BOUNDED ps   &    |- BOUNDED ch   =>    |- BOUNDED ( ph /\ ps /\ ch )
Theorem	bdth 12610	A truth (a (closed) theorem) is a bounded formula. (Contributed by BJ, 6-Oct-2019.)
|- ph   =>    |- BOUNDED ph
Theorem	bdtru 12611	The truth value T. is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED T.
Theorem	bdfal 12612	The truth value F. is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED F.
Theorem	bdnth 12613	A falsity is a bounded formula. (Contributed by BJ, 6-Oct-2019.)
|- -. ph   =>    |- BOUNDED ph
Theorem	bdnthALT 12614	Alternate proof of bdnth 12613 not using bdfal 12612. Then, bdfal 12612 can be proved from this theorem, using fal 1306. The total number of proof steps would be 17 (for bdnthALT 12614) + 3 = 20, which is more than 8 (for bdfal 12612) + 9 (for bdnth 12613) = 17. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- -. ph   =>    |- BOUNDED ph
Theorem	bdxor 12615	The exclusive disjunction of two bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/_ ps )
Theorem	bj-bdcel 12616*	Boundedness of a membership formula. (Contributed by BJ, 8-Dec-2019.)
|- BOUNDED y = A   =>    |- BOUNDED A e. x
Theorem	bdab 12617	Membership in a class defined by class abstraction using a bounded formula, is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED x e. { y | ph }
Theorem	bdcdeq 12618	Conditional equality of a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED CondEq ( x = y -> ph )
9.2.6.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 12620. 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 12654), one can prove the boundedness of any concrete term using only setvars and bounded formulas, for instance, |- BOUNDED ph => |- BOUNDED <. { x | ph } , ( { y , suc z } X. <. t , (/) >. ) >.. 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 A => |- BOUNDED { A }.
Syntax	wbdc 12619	Syntax for the predicate BOUNDED.
wff BOUNDED A
Definition	df-bdc 12620*	Define a bounded class as one such that membership in this class is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
|- (BOUNDED A <-> A. xBOUNDED x e. A )
Theorem	bdceq 12621	Equality property for the predicate BOUNDED. (Contributed by BJ, 3-Oct-2019.)
|- A = B   =>    |- (BOUNDED A <-> BOUNDED B )
Theorem	bdceqi 12622	A class equal to a bounded one is bounded. Note the use of ax-ext 2082. See also bdceqir 12623. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- A = B   =>    |- BOUNDED B
Theorem	bdceqir 12623	A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 12622) equality in the hypothesis, to work better with definitions ( B is the definiendum that one wants to prove bounded; see comment of bd0r 12604). (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- B = A   =>    |- BOUNDED B
Theorem	bdel 12624*	The belonging of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
|- (BOUNDED A -> BOUNDED x e. A )
Theorem	bdeli 12625*	Inference associated with bdel 12624. Its converse is bdelir 12626. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED x e. A
Theorem	bdelir 12626*	Inference associated with df-bdc 12620. Its converse is bdeli 12625. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED x e. A   =>    |- BOUNDED A
Theorem	bdcv 12627	A setvar is a bounded class. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED x
Theorem	bdcab 12628	A class defined by class abstraction using a bounded formula is bounded. (Contributed by BJ, 6-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED { x | ph }
Theorem	bdph 12629	A formula which defines (by class abstraction) a bounded class is bounded. (Contributed by BJ, 6-Oct-2019.)
|- BOUNDED { x | ph }   =>    |- BOUNDED ph
Theorem	bds 12630*	Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 12601; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 12601. (Contributed by BJ, 19-Nov-2019.)
|- BOUNDED ph   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- BOUNDED ps
Theorem	bdcrab 12631*	A class defined by restricted abstraction from a bounded class and a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED ph   =>    |- BOUNDED { x e. A | ph }
Theorem	bdne 12632	Inequality of two setvars is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED x =/= y
Theorem	bdnel 12633*	Non-membership of a setvar in a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED x e/ A
Theorem	bdreu 12634*	Boundedness of existential uniqueness. Remark regarding restricted quantifiers: the formula A. x e. A ph need not be bounded even if A and ph are. Indeed, _V is bounded by bdcvv 12636, and |- ( A. x e. _V ph <-> A. x ph ) (in minimal propositional calculus), so by bd0 12603, if A. x e. _V ph were bounded when ph is bounded, then A. x ph would be bounded as well when ph is bounded, which is not the case. The same remark holds with E. , E! , E*. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED E! x e. y ph
Theorem	bdrmo 12635*	Boundedness of existential at-most-one. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED E* x e. y ph
Theorem	bdcvv 12636	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 12637	A formula resulting from proper substitution of a setvar for a setvar in a bounded formula is bounded. See also bdsbcALT 12638. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED [. y / x ]. ph
Theorem	bdsbcALT 12638	Alternate proof of bdsbc 12637. (Contributed by BJ, 16-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- BOUNDED ph   =>    |- BOUNDED [. y / x ]. ph
Theorem	bdccsb 12639	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 A   =>    |- BOUNDED [_ y / x ]_ A
Theorem	bdcdif 12640	The difference of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- BOUNDED ( A \ B )
Theorem	bdcun 12641	The union of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- BOUNDED ( A u. B )
Theorem	bdcin 12642	The intersection of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- BOUNDED ( A i^i B )
Theorem	bdss 12643	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 A   =>    |- BOUNDED x C_ A
Theorem	bdcnul 12644	The empty class is bounded. See also bdcnulALT 12645. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED (/)
Theorem	bdcnulALT 12645	Alternate proof of bdcnul 12644. Similarly, for the next few theorems proving boundedness of a class, one can either use their definition followed by bdceqir 12623, or use the corresponding characterizations of its elements followed by bdelir 12626. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- BOUNDED (/)
Theorem	bdeq0 12646	Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED x = (/)
Theorem	bj-bd0el 12647	Boundedness of the formula "the empty set belongs to the setvar x". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED (/) e. x
Theorem	bdcpw 12648	The power class of a bounded class is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED ~P A
Theorem	bdcsn 12649	The singleton of a setvar is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED { x }
Theorem	bdcpr 12650	The pair of two setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED { x , y }
Theorem	bdctp 12651	The unordered triple of three setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED { x , y , z }
Theorem	bdsnss 12652*	Inclusion of a singleton of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED { x } C_ A
Theorem	bdvsn 12653*	Equality of a setvar with a singleton of a setvar is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED x = { y }
Theorem	bdop 12654	The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED <. x , y >.
Theorem	bdcuni 12655	The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.)
|- BOUNDED U. x
Theorem	bdcint 12656	The intersection of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED |^| x
Theorem	bdciun 12657*	The indexed union of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED U_ x e. y A
Theorem	bdciin 12658*	The indexed intersection of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED |^|_ x e. y A
Theorem	bdcsuc 12659	The successor of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED suc x
Theorem	bdeqsuc 12660*	Boundedness of the formula expressing that a setvar is equal to the successor of another. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED x = suc y
Theorem	bj-bdsucel 12661	Boundedness of the formula "the successor of the setvar x belongs to the setvar y". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED suc x e. y
Theorem	bdcriota 12662*	A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.)
|- BOUNDED ph   &    |- E! x e. y ph   =>    |- BOUNDED ( iota_ x e. y ph )
9.2.7  CZF: Bounded separation In this section, we state the axiom scheme of bounded separation, which is part of CZF set theory.
Axiom	ax-bdsep 12663*	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 3986. (Contributed by BJ, 5-Oct-2019.)
|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsep1 12664*	Version of ax-bdsep 12663 without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.)
|- BOUNDED ph   =>    |- E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsep2 12665*	Version of ax-bdsep 12663 with one disjoint variable condition removed and without initial universal quantifier. Use bdsep1 12664 when sufficient. (Contributed by BJ, 5-Oct-2019.)
|- BOUNDED ph   =>    |- E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsepnft 12666*	Closed form of bdsepnf 12667. Version of ax-bdsep 12663 with one disjoint variable condition removed, the other disjoint variable condition replaced by a non-freeness antecedent, and without initial universal quantifier. Use bdsep1 12664 when sufficient. (Contributed by BJ, 19-Oct-2019.)
|- BOUNDED ph   =>    |- ( A. x F/ b ph -> E. b A. x ( x e. b <-> ( x e. a /\ ph ) ) )
Theorem	bdsepnf 12667*	Version of ax-bdsep 12663 with one disjoint variable condition removed, the other disjoint variable condition replaced by a non-freeness hypothesis, and without initial universal quantifier. See also bdsepnfALT 12668. Use bdsep1 12664 when sufficient. (Contributed by BJ, 5-Oct-2019.)
|- F/ b ph   &    |- BOUNDED ph   =>    |- E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsepnfALT 12668*	Alternate proof of bdsepnf 12667, not using bdsepnft 12666. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ b ph   &    |- BOUNDED ph   =>    |- E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdzfauscl 12669*	Closed form of the version of zfauscl 3988 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.)
|- BOUNDED ph   =>    |- ( A e. V -> E. y A. x ( x e. y <-> ( x e. A /\ ph ) ) )
Theorem	bdbm1.3ii 12670*	Bounded version of bm1.3ii 3989. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- BOUNDED ph   &    |- E. x A. y ( ph -> y e. x )   =>    |- E. x A. y ( y e. x <-> ph )
Theorem	bj-axemptylem 12671*	Lemma for bj-axempty 12672 and bj-axempty2 12673. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3994 instead. (New usage is discouraged.)
|- E. x A. y ( y e. x -> F. )
Theorem	bj-axempty 12672*	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 3993. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3994 instead. (New usage is discouraged.)
|- E. x A. y e. x F.
Theorem	bj-axempty2 12673*	Axiom of the empty set from bounded separation, alternate version to bj-axempty 12672. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3994 instead. (New usage is discouraged.)
|- E. x A. y -. y e. x
Theorem	bj-nalset 12674*	nalset 3998 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. E. x A. y y e. x
Theorem	bj-vprc 12675	vprc 4000 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. _V e. _V
Theorem	bj-nvel 12676	nvel 4001 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. _V e. A
Theorem	bj-vnex 12677	vnex 3999 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. E. x x = _V
Theorem	bdinex1 12678	Bounded version of inex1 4002. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   &    |- A e. _V   =>    |- ( A i^i B ) e. _V
Theorem	bdinex2 12679	Bounded version of inex2 4003. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   &    |- A e. _V   =>    |- ( B i^i A ) e. _V
Theorem	bdinex1g 12680	Bounded version of inex1g 4004. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   =>    |- ( A e. V -> ( A i^i B ) e. _V )
Theorem	bdssex 12681	Bounded version of ssex 4005. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &    |- B e. _V   =>    |- ( A C_ B -> A e. _V )
Theorem	bdssexi 12682	Bounded version of ssexi 4006. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &    |- B e. _V   &    |- A C_ B   =>    |- A e. _V
Theorem	bdssexg 12683	Bounded version of ssexg 4007. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   =>    |- ( ( A C_ B /\ B e. C ) -> A e. _V )
Theorem	bdssexd 12684	Bounded version of ssexd 4008. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ( ph -> B e. C )   &    |- ( ph -> A C_ B )   &    |- BOUNDED A   =>    |- ( ph -> A e. _V )
Theorem	bdrabexg 12685*	Bounded version of rabexg 4011. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED ph   &    |- BOUNDED A   =>    |- ( A e. V -> { x e. A | ph } e. _V )
Theorem	bj-inex 12686	The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- ( ( A e. V /\ B e. W ) -> ( A i^i B ) e. _V )
Theorem	bj-intexr 12687	intexr 4015 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- ( |^| A e. _V -> A =/= (/) )
Theorem	bj-intnexr 12688	intnexr 4016 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- ( |^| A = _V -> -. |^| A e. _V )
Theorem	bj-zfpair2 12689	Proof of zfpair2 4070 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- { x , y } e. _V
Theorem	bj-prexg 12690	Proof of prexg 4071 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- ( ( A e. V /\ B e. W ) -> { A , B } e. _V )
Theorem	bj-snexg 12691	snexg 4048 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- ( A e. V -> { A } e. _V )
Theorem	bj-snex 12692	snex 4049 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- A e. _V   =>    |- { A } e. _V
Theorem	bj-sels 12693*	If a class is a set, then it is a member of a set. (Copied from set.mm.) (Contributed by BJ, 3-Apr-2019.)
|- ( A e. V -> E. x A e. x )
Theorem	bj-axun2 12694*	axun2 4295 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
|- E. y A. z ( z e. y <-> E. w ( z e. w /\ w e. x ) )
Theorem	bj-uniex2 12695*	uniex2 4296 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
|- E. y y = U. x
Theorem	bj-uniex 12696	uniex 4297 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   =>    |- U. A e. _V
Theorem	bj-uniexg 12697	uniexg 4299 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ( A e. V -> U. A e. _V )
Theorem	bj-unex 12698	unex 4300 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   &    |- B e. _V   =>    |- ( A u. B ) e. _V
Theorem	bdunexb 12699	Bounded version of unexb 4301. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- ( ( A e. _V /\ B e. _V ) <-> ( A u. B ) e. _V )
Theorem	bj-unexg 12700	unexg 4302 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )