P. 463 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46201-46300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ixpssixp 46201	Subclass theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶)
Theorem	ballss3 46202*	A sufficient condition for a ball being a subset. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑋))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) → 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑃(ball‘𝐷)𝑅) ⊆ 𝐴)
Theorem	iunincfi 46203*	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 46204	If it's not a subclass, it's not a subclass of a smaller one. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ ((¬ 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐵) → ¬ 𝐴 ⊆ 𝐶)
Theorem	rexanuz3 46205*	Combine two different upper integer properties into one, for a single integer. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑗𝜑    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜒)    &   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜓)    &   ⊢ (𝑘 = 𝑗 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑘 = 𝑗 → (𝜓 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 (𝜃 ∧ 𝜏))
Theorem	cbvmpo2 46206*	Rule to change the second bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑤𝐴    &   ⊢ Ⅎ𝑤𝐶    &   ⊢ Ⅎ𝑦𝐸    &   ⊢ (𝑦 = 𝑤 → 𝐶 = 𝐸)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐸)
Theorem	cbvmpo1 46207*	Rule to change the first bound variable in a maps-to function, using implicit substitution. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑥𝐸    &   ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸)
Theorem	eliuniin 46208*	Indexed union of indexed intersections. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷    ⇒   ⊢ (𝑍 ∈ 𝑉 → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷))
Theorem	ssabf 46209	Subclass of a class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
Theorem	pssnssi 46210	A proper subclass does not include the other class. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐴 ⊊ 𝐵    ⇒   ⊢ ¬ 𝐵 ⊆ 𝐴
Theorem	rabidim2 46211	Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝜑)
Theorem	eluni2f 46212*	Membership in class union. Restricted quantifier version. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)
Theorem	eliin2f 46213*	Membership in indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
Theorem	nssd 46214	Negation of subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ¬ 𝐴 ⊆ 𝐵)
Theorem	iineq12dv 46215*	Equality deduction for indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Remove DV conditions. (Revised by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷)
Theorem	supxrcld 46216	The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ*)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ*, < ) ∈ ℝ*)
Theorem	elrestd 46217	A sufficient condition for being an open set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐽 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐽)    &   ⊢ 𝐴 = (𝑋 ∩ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐽 ↾t 𝐵))
Theorem	eliuniincex 46218*	Counterexample to show that the additional conditions in eliuniin 46208 and eliuniin2 46229 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 46219*	Counterexample to show that the additional conditions in eliin 4955 and eliin2 46225 are actually needed. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐴 = V    &   ⊢ 𝐵 = ∅    ⇒   ⊢ ¬ (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)
Theorem	eliinid 46220*	Membership in an indexed intersection implies membership in any intersected set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ ((𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐶)
Theorem	abssf 46221	Class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ ({𝑥 ∣ 𝜑} ⊆ 𝐴 ↔ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴))
Theorem	supxrubd 46222	A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ 𝑆 = sup(𝐴, ℝ*, < )    ⇒   ⊢ (𝜑 → 𝐵 ≤ 𝑆)
Theorem	ssrabf 46223	Subclass of a restricted class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 𝜑))
Theorem	ssrabdf 46224	Subclass of a restricted class abstraction (deduction form). (Contributed by Glauco Siliprandi, 5-Jan-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝜓)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ {𝑥 ∈ 𝐴 ∣ 𝜓})
Theorem	eliin2 46225*	Membership in indexed intersection. See eliincex 46219 for a counterexample showing that the precondition 𝐵 ≠ ∅ cannot be simply dropped. eliin 4955 uses an alternative precondition (and it doesn't have a disjoint var constraint between 𝐵 and 𝑥; see eliin2f 46213). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
Theorem	ssrab2f 46226	Subclass relation for a restricted class. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
Theorem	restuni3 46227	The underlying set of a subspace induced by the subspace operator ↾t. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) = (∪ 𝐴 ∩ 𝐵))
Theorem	rabssf 46228	Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑥 ∈ 𝐵))
Theorem	eliuniin2 46229*	Indexed union of indexed intersections. See eliincex 46219 for a counterexample showing that the precondition 𝐶 ≠ ∅ cannot be simply dropped. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝐶    &   ⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷    ⇒   ⊢ (𝐶 ≠ ∅ → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷))
Theorem	restuni4 46230	The underlying set of a subspace induced by the ↾t operator. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ⊆ ∪ 𝐴)    ⇒   ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) = 𝐵)
Theorem	restuni6 46231	The underlying set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) = (∪ 𝐴 ∩ 𝐵))
Theorem	restuni5 46232	The underlying set of a subspace induced by the ↾t operator. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
Theorem	unirestss 46233	The union of an elementwise intersection is a subset of the underlying set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∪ (𝐴 ↾t 𝐵) ⊆ ∪ 𝐴)
Theorem	iniin1 46234*	Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ≠ ∅ → (∩ 𝑥 ∈ 𝐴 𝐶 ∩ 𝐵) = ∩ 𝑥 ∈ 𝐴 (𝐶 ∩ 𝐵))
Theorem	iniin2 46235*	Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝐴 ≠ ∅ → (𝐵 ∩ ∩ 𝑥 ∈ 𝐴 𝐶) = ∩ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶))
Theorem	cbvrabv2 46236*	A more general version of cbvrabv 3422. Usage of this theorem is discouraged because it depends on ax-13 2401. Use of cbvrabv2w 46237 is preferred. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓}
Theorem	cbvrabv2w 46237*	A more general version of cbvrabv 3422. Version of cbvrabv2 46236 with a disjoint variable condition, which does not require ax-13 2401. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Revised by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ 𝜓}
Theorem	iinssiin 46238	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ ∩ 𝑥 ∈ 𝐴 𝐶)
Theorem	eliind2 46239*	Membership in indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐴 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶)
Theorem	iinssd 46240*	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	rabbida2 46241	Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	iinexd 46242*	The existence of an indexed union. 𝑥 is normally a free-variable parameter in 𝐵, which should be read 𝐵(𝑥). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ V)
Theorem	rabexf 46243	Separation Scheme in terms of a restricted class abstraction. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐴    &   ⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V
Theorem	rabbida3 46244	Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
Theorem	r19.36vf 46245	Restricted quantifier version of one direction of 19.36 2266. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → 𝜓))
Theorem	raleqd 46246	Equality deduction for restricted universal quantifier. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
Theorem	iinssf 46247	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐶    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	iinssdf 46248	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝑋    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	resabs2i 46249	Absorption law for restriction. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ 𝐵 ⊆ 𝐶    ⇒   ⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ 𝐵)
Theorem	ssdf2 46250	A sufficient condition for a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	rabssd 46251	Restricted class abstraction in a subclass relationship. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒) → 𝑥 ∈ 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜒} ⊆ 𝐵)
Theorem	rexnegd 46252	Minus a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → -e𝐴 = -𝐴)
Theorem	rexlimd3 46253	* Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
Theorem	nel1nelini 46254	Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ ¬ 𝐴 ∈ 𝐵    ⇒   ⊢ ¬ 𝐴 ∈ (𝐵 ∩ 𝐶)
Theorem	nel2nelini 46255	Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ ¬ 𝐴 ∈ 𝐶    ⇒   ⊢ ¬ 𝐴 ∈ (𝐵 ∩ 𝐶)
Theorem	eliunid 46256*	Membership in indexed union. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	reximdd 46257	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒)
Theorem	inopnd 46258	The intersection of two open sets of a topology is an open set. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ 𝐽)
Theorem	ss2rabdf 46259	Deduction of restricted abstraction subclass from implication. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	restopn3 46260	If 𝐴 is open, then 𝐴 is open in the restriction to itself. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ∈ (𝐽 ↾t 𝐴))
Theorem	restopnssd 46261	A topology restricted to an open set is a subset of the original topology. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    ⇒   ⊢ (𝜑 → (𝐽 ↾t 𝐴) ⊆ 𝐽)
Theorem	restsubel 46262	A subset belongs in the space it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ (𝜑 → 𝐽 ∈ 𝑉)    &   ⊢ (𝜑 → ∪ 𝐽 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐽 ↾t 𝐴))
Theorem	toprestsubel 46263	A subset is open in the topology it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐽)    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝐽 ↾t 𝐴))
Theorem	rabidd 46264	An "identity" law of concretion for restricted abstraction. Special case of Definition 2.1 of [Quine] p. 16. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ (𝜑 → 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜒})
Theorem	iunssdf 46265	Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	iinss2d 46266	Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
Theorem	r19.3rzf 46267	Restricted quantification of wff not containing quantified variable. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))
Theorem	r19.28zf 46268	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)))
Theorem	iindif2f 46269	Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws". (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (𝐵 ∖ ∪ 𝑥 ∈ 𝐴 𝐶))
Theorem	ralfal 46270	Two ways of expressing empty set. (Contributed by Glauco Siliprandi, 24-Jan-2024.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 = ∅ ↔ ∀𝑥 ∈ 𝐴 ⊥)
Theorem	archd 46271*	Archimedean property of real numbers. For any real number, there is an integer greater than it. Theorem I.29 of [Apostol] p. 26. (Contributed by Glauco Siliprandi, 1-Feb-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ 𝐴 < 𝑛)
Theorem	nimnbi 46272	If an implication is false, the biconditional is false. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ ¬ (𝜑 → 𝜓)    ⇒   ⊢ ¬ (𝜑 ↔ 𝜓)
Theorem	nimnbi2 46273	If an implication is false, the biconditional is false. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ ¬ (𝜓 → 𝜑)    ⇒   ⊢ ¬ (𝜑 ↔ 𝜓)
Theorem	notbicom 46274	Commutative law for the negation of a biconditional. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ ¬ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ (𝜓 ↔ 𝜑)
Theorem	rexeqif 46275	Equality inference for restricted existential quantifier. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)
Theorem	rspced 46276	Restricted existential specialization, using implicit substitution. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
21.47.2  Functions
Theorem	fnresdmss 46277	A function does not change when restricted to a set that contains its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐹 ↾ 𝐵) = 𝐹)
Theorem	fmptsnxp 46278*	Maps-to notation and Cartesian product for a singleton function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑥 ∈ {𝐴} ↦ 𝐵) = ({𝐴} × {𝐵}))
Theorem	fvmpt2bd 46279*	Value of a function given by the maps-to notation. Deduction version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐹‘𝑥) = 𝐵)
Theorem	rnmptfi 46280*	The range of a function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ (𝐵 ∈ Fin → ran 𝐴 ∈ Fin)
Theorem	fresin2 46281	Restriction of a function with respect to the intersection with its domain. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ↾ (𝐶 ∩ 𝐴)) = (𝐹 ↾ 𝐶))
Theorem	ffi 46282	A function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ Fin) → 𝐹 ∈ Fin)
Theorem	suprnmpt 46283*	An explicit bound for the range of a bounded function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ 𝐶 = sup(ran 𝐹, ℝ, < )    ⇒   ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶))
Theorem	rnffi 46284	The range of a function with finite domain is finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ Fin) → ran 𝐹 ∈ Fin)
Theorem	mptelpm 46285*	A function in maps-to notation is a partial map . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (𝐶 ↑pm 𝐷))
Theorem	rnmptpr 46286*	Range of a function defined on an unordered pair. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐶)    &   ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸)    ⇒   ⊢ (𝜑 → ran 𝐹 = {𝐷, 𝐸})
Theorem	resmpti 46287*	Restriction of the mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝐵 ⊆ 𝐴    ⇒   ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ↾ 𝐵) = (𝑥 ∈ 𝐵 ↦ 𝐶)
Theorem	founiiun 46288*	Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐹:𝐴–onto→𝐵 → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥))
Theorem	rnresun 46289	Distribution law for range of a restriction over a union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ran (𝐹 ↾ (𝐴 ∪ 𝐵)) = (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵))
Theorem	elrnmptf 46290	The range of a function in maps-to notation. Same as elrnmpt 5939, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝐶    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
Theorem	rnmptssrn 46291*	Inclusion relation for two ranges expressed in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐶 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ran (𝑦 ∈ 𝐶 ↦ 𝐷))
Theorem	disjf1 46292*	A 1 to 1 mapping built from disjoint, nonempty sets. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → 𝐹:𝐴–1-1→𝑉)
Theorem	rnsnf 46293	The range of a function whose domain is a singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:{𝐴}⟶𝐵)    ⇒   ⊢ (𝜑 → ran 𝐹 = {(𝐹‘𝐴)})
Theorem	wessf1ornlem 46294*	Given a function 𝐹 on a well-ordered domain 𝐴 there exists a subset of 𝐴 such that 𝐹 restricted to such subset is injective and onto the range of 𝐹 (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹)
Theorem	wessf1orn 46295*	Given a function 𝐹 on a well-ordered domain 𝐴 there exists a subset of 𝐴 such that 𝐹 restricted to such subset is injective and onto the range of 𝐹 (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran 𝐹)
Theorem	nelrnres 46296	If 𝐴 is not in the range, it is not in the range of any restriction. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (¬ 𝐴 ∈ ran 𝐵 → ¬ 𝐴 ∈ ran (𝐵 ↾ 𝐶))
Theorem	disjrnmpt2 46297*	Disjointness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran 𝐹 𝑦)
Theorem	elrnmpt1sf 46298*	Elementhood in an image set. Same as elrnmpt1s 5940, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝐶    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶)    ⇒   ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹)
Theorem	founiiun0 46299*	Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥))
Theorem	disjf1o 46300*	A bijection built from disjoint sets. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅}    &   ⊢ 𝐷 = (ran 𝐹 ∖ {∅})    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶–1-1-onto→𝐷)