P. 438 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43701-43800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rzalf 43701	A version of rzal 4509 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥 𝐴 = ∅    ⇒   ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	fvelrnbf 43702	A version of fvelrnb 6953 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
Theorem	rfcnpre1 43703	If F is a continuous function with respect to the standard topology, then the preimage A of the values greater than a given extended real B is an open set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐴 = {𝑥 ∈ 𝑋 ∣ 𝐵 < (𝐹‘𝑥)}    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐽)
Theorem	ubelsupr 43704*	If U belongs to A and U is an upper bound, then U is the sup of A. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝑈 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑈) → 𝑈 = sup(𝐴, ℝ, < ))
Theorem	fsumcnf 43705*	A finite sum of functions to complex numbers from a common topological space is continuous, without disjoint var constraint x ph. The class expression for B normally contains free variables k and x to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾))
Theorem	mulltgt0 43706	The product of a negative and a positive number is negative. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 < 0) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 · 𝐵) < 0)
Theorem	rspcegf 43707	A version of rspcev 3613 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	rabexgf 43708	A version of rabexg 5332 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	fcnre 43709	A function continuous with respect to the standard topology, is a real mapping. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
Theorem	sumsnd 43710*	A sum of a singleton is the term. The deduction version of sumsn 15692. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (𝜑 → Ⅎ𝑘𝐵)    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ {𝑀}𝐴 = 𝐵)
Theorem	evthf 43711*	A version of evth 24475 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑦𝐹    &   ⊢ Ⅎ𝑥𝑋    &   ⊢ Ⅎ𝑦𝑋    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥))
Theorem	cnfex 43712	The class of continuous functions between two topologies is a set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) ∈ V)
Theorem	fnchoice 43713*	For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
Theorem	refsumcn 43714*	A finite sum of continuous real functions, from a common topological space, is continuous. The class expression for B normally contains free variables k and x to index it. See fsumcn 24386 for the analogous theorem on continuous complex functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾))
Theorem	rfcnpre2 43715	If 𝐹 is a continuous function with respect to the standard topology, then the preimage A of the values smaller than a given extended real 𝐵, is an open set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐴 = {𝑥 ∈ 𝑋 ∣ (𝐹‘𝑥) < 𝐵}    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐽)
Theorem	cncmpmax 43716*	When the hypothesis for the extreme value theorem hold, then the sup of the range of the function belongs to the range, it is real and it an upper bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑇 ≠ ∅)    ⇒   ⊢ (𝜑 → (sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ∧ sup(ran 𝐹, ℝ, < ) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ sup(ran 𝐹, ℝ, < )))
Theorem	rfcnpre3 43717*	If F is a continuous function with respect to the standard topology, then the preimage A of the values greater than or equal to a given real B is a closed set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐴 = {𝑡 ∈ 𝑇 ∣ 𝐵 ≤ (𝐹‘𝑡)}    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽))
Theorem	rfcnpre4 43718*	If F is a continuous function with respect to the standard topology, then the preimage A of the values less than or equal to a given real B is a closed set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐴 = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ 𝐵}    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽))
Theorem	sumpair 43719*	Sum of two distinct complex values. The class expression for 𝐴 and 𝐵 normally contain free variable 𝑘 to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (𝜑 → Ⅎ𝑘𝐷)    &   ⊢ (𝜑 → Ⅎ𝑘𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐴) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐵) → 𝐶 = 𝐸)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 + 𝐸))
Theorem	rfcnnnub 43720*	Given a real continuous function 𝐹 defined on a compact topological space, there is always a positive integer that is a strict upper bound of its range. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ (𝜑 → 𝑇 ≠ ∅)    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) < 𝑛)
Theorem	refsum2cnlem1 43721*	This is the core Lemma for refsum2cn 43722: the sum of two continuous real functions (from a common topological space) is continuous. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐺    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐴 = (𝑘 ∈ {1, 2} ↦ if(𝑘 = 1, 𝐹, 𝐺))    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ (𝐽 Cn 𝐾))
Theorem	refsum2cn 43722*	The sum of two continuus real functions (from a common topological space) is continuous. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐺    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ (𝐽 Cn 𝐾))
Theorem	adantlllr 43723	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	3adantlr3 43724	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜂)) ∧ 𝜃) → 𝜏)
Theorem	3adantll2 43725	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜂 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	3adantll3 43726	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜂) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	ssnel 43727	If not element of a set, then not element of a subset. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐵) → ¬ 𝐶 ∈ 𝐴)
Theorem	elabrexg 43728*	Elementhood in an image set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵})
Theorem	sncldre 43729	A singleton is closed w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℝ → {𝐴} ∈ (Clsd‘(topGen‘ran (,))))
Theorem	n0p 43730	A polynomial with a nonzero coefficient is not the zero polynomial. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ ((𝑃 ∈ (Poly‘ℤ) ∧ 𝑁 ∈ ℕ0 ∧ ((coeff‘𝑃)‘𝑁) ≠ 0) → 𝑃 ≠ 0𝑝)
Theorem	pm2.65ni 43731	Inference rule for proof by contradiction. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (¬ 𝜑 → 𝜓)    &   ⊢ (¬ 𝜑 → ¬ 𝜓)    ⇒   ⊢ 𝜑
Theorem	pwssfi 43732	Every element of the power set of 𝐴 is finite if and only if 𝐴 is finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ 𝒫 𝐴 ⊆ Fin))
Theorem	iuneq2df 43733	Equality deduction for indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	nnfoctb 43734*	There exists a mapping from ℕ onto any (nonempty) countable set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–onto→𝐴)
Theorem	ssinss1d 43735	Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	elpwinss 43736	An element of the powerset of 𝐵 intersected with anything, is a subset of 𝐵. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵)
Theorem	unidmex 43737	If 𝐹 is a set, then ∪ dom 𝐹 is a set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝑋 = ∪ dom 𝐹    ⇒   ⊢ (𝜑 → 𝑋 ∈ V)
Theorem	ndisj2 43738*	A non-disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (¬ Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ (𝐵 ∩ 𝐶) ≠ ∅))
Theorem	zenom 43739	The set of integer numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ℤ ≈ ω
Theorem	uzwo4 43740*	Well-ordering principle: any nonempty subset of an upper set of integers has the least element. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑗𝜓    &   ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ ∃𝑗 ∈ 𝑆 𝜑) → ∃𝑗 ∈ 𝑆 (𝜑 ∧ ∀𝑘 ∈ 𝑆 (𝑘 < 𝑗 → ¬ 𝜓)))
Theorem	unisn0 43741	The union of the singleton of the empty set is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ∪ {∅} = ∅
Theorem	ssin0 43742	If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → (𝐶 ∩ 𝐷) = ∅)
Theorem	inabs3 43743	Absorption law for intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐶 ⊆ 𝐵 → ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ 𝐶))
Theorem	pwpwuni 43744	Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵))
Theorem	disjiun2 43745*	In a disjoint collection, an indexed union is disjoint from an additional term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴 ∖ 𝐶))    &   ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐸)    ⇒   ⊢ (𝜑 → (∪ 𝑥 ∈ 𝐶 𝐵 ∩ 𝐸) = ∅)
Theorem	0pwfi 43746	The empty set is in any power set, and it's finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ∅ ∈ (𝒫 𝐴 ∩ Fin)
Theorem	ssinss2d 43747	Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	zct 43748	The set of integer numbers is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ℤ ≼ ω
Theorem	pwfin0 43749	A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝒫 𝐴 ∩ Fin) ≠ ∅
Theorem	uzct 43750	An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝑍 = (ℤ≥‘𝑁)    ⇒   ⊢ 𝑍 ≼ ω
Theorem	iunxsnf 43751*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝐶    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶
Theorem	fiiuncl 43752*	If a set is closed under the union of two sets, then it is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (𝑦 ∪ 𝑧) ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷)
Theorem	iunp1 43753*	The addition of the next set to a union indexed by a finite set of sequential integers. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝐵    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ (𝑀...(𝑁 + 1))𝐴 = (∪ 𝑘 ∈ (𝑀...𝑁)𝐴 ∪ 𝐵))
Theorem	fiunicl 43754*	If a set is closed under the union of two sets, then it is closed under finite union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∪ 𝑦) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝐴)
Theorem	ixpeq2d 43755	Equality theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	disjxp1 43756*	The sets of a cartesian product are disjoint if the sets in the first argument are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 (𝐵 × 𝐶))
Theorem	disjsnxp 43757*	The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Disj 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
Theorem	eliind 43758*	Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐵)    &   ⊢ (𝑥 = 𝐾 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐷)
Theorem	rspcef 43759	Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	inn0f 43760	A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	ixpssmapc 43761*	An infinite Cartesian product is a subset of set exponentiation. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐶 ↑m 𝐴))
Theorem	inn0 43762*	A nonempty intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ ((𝐴 ∩ 𝐵) ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)
Theorem	elintd 43763*	Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵)
Theorem	ssdf 43764*	A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	brneqtrd 43765	Substitution of equal classes into the negation of a binary relation. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → ¬ 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ¬ 𝐴𝑅𝐶)
Theorem	ssnct 43766	A set containing an uncountable set is itself uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → ¬ 𝐴 ≼ ω)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐵 ≼ ω)
Theorem	ssuniint 43767*	Sufficient condition for being a subclass of the union of an intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ ∪ ∩ 𝐵)
Theorem	elintdv 43768*	Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝑥)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ∩ 𝐵)
Theorem	ssd 43769*	A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	ralimralim 43770	Introducing any antecedent in a restricted universal quantification. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑))
Theorem	snelmap 43771	Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → (𝐴 × {𝑥}) ∈ (𝐵 ↑m 𝐴))    ⇒   ⊢ (𝜑 → 𝑥 ∈ 𝐵)
Theorem	xrnmnfpnf 43772	An extended real that is neither real nor minus infinity, is plus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ -∞)    ⇒   ⊢ (𝜑 → 𝐴 = +∞)
Theorem	nelrnmpt 43773*	Non-membership in the range of a function in maps-to notaion. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐶 ∈ ran 𝐹)
Theorem	iuneq1i 43774*	Equality theorem for indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶
Theorem	nssrex 43775*	Negation of subclass relationship. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)
Theorem	ssinc 43776*	Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑀) ⊆ (𝐹‘𝑁))
Theorem	ssdec 43777*	Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘(𝑚 + 1)) ⊆ (𝐹‘𝑚))    ⇒   ⊢ (𝜑 → (𝐹‘𝑁) ⊆ (𝐹‘𝑀))
Theorem	elixpconstg 43778*	Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵))
Theorem	iineq1d 43779*	Equality theorem for indexed intersection. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶)
Theorem	metpsmet 43780	A metric is a pseudometric. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋))
Theorem	ixpssixp 43781	Subclass theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶)
Theorem	ballss3 43782*	A sufficient condition for a ball being a subset. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑋))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) → 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑃(ball‘𝐷)𝑅) ⊆ 𝐴)
Theorem	iunincfi 43783*	Given a sequence of increasing sets, the union of a finite subsequence, is its last element. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))    ⇒   ⊢ (𝜑 → ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) = (𝐹‘𝑁))
Theorem	nsstr 43784	If it's not a subclass, it's not a subclass of a smaller one. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ ((¬ 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐵) → ¬ 𝐴 ⊆ 𝐶)
Theorem	rexanuz3 43785*	Combine two different upper integer properties into one, for a single integer. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑗𝜑    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜒)    &   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓)    &   ⊢ (𝑘 = 𝑗 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑘 = 𝑗 → (𝜓 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝜃 ∧ 𝜏))
Theorem	cbvmpo2 43786*	Rule to change the second bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑤𝐴    &   ⊢ Ⅎ𝑤𝐶    &   ⊢ Ⅎ𝑦𝐸    &   ⊢ (𝑦 = 𝑤 → 𝐶 = 𝐸)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐸)
Theorem	cbvmpo1 43787*	Rule to change the first bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑥𝐸    &   ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸)
Theorem	eliuniin 43788*	Indexed union of indexed intersections. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷    ⇒   ⊢ (𝑍 ∈ 𝑉 → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷))
Theorem	ssabf 43789	Subclass of a class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
Theorem	pssnssi 43790	A proper subclass does not include the other class. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐴 ⊊ 𝐵    ⇒   ⊢ ¬ 𝐵 ⊆ 𝐴
Theorem	rabidim2 43791	Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝜑)
Theorem	eluni2f 43792*	Membership in class union. Restricted quantifier version. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)
Theorem	eliin2f 43793*	Membership in indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
Theorem	nssd 43794	Negation of subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐴 ⊆ 𝐵)
Theorem	iineq12dv 43795*	Equality deduction for indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷)
Theorem	supxrcld 43796	The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ*)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*)
Theorem	elrestd 43797	A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐽 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ 𝐴 = (𝑋 ∩ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐽 ↾t 𝐵))
Theorem	eliuniincex 43798*	Counterexample to show that the additional conditions in eliuniin 43788 and eliuniin2 43809 are actually needed. Notice that the definition of 𝐴 is not even needed (it can be any class). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐵 = {∅}    &   ⊢ 𝐶 = ∅    &   ⊢ 𝐷 = ∅    &   ⊢ 𝑍 = V    ⇒   ⊢ ¬ (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)
Theorem	eliincex 43799*	Counterexample to show that the additional conditions in eliin 5003 and eliin2 43805 are actually needed. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐴 = V    &   ⊢ 𝐵 = ∅    ⇒   ⊢ ¬ (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)
Theorem	eliinid 43800*	Membership in an indexed intersection implies membership in any intersected set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ ((𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐶)