P. 372 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37101-37200   *Has distinct variable group(s)

Type	Label	Description
Statement
21.12.18  Forward difference
Syntax	cfwddif 37101	Declare the syntax for the forward difference operator.
class △
Definition	df-fwddif 37102*	Define the forward difference operator. This is a discrete analogue of the derivative operator. Definition 2.42 of [GramKnuthPat], p. 47. (Contributed by Scott Fenton, 18-May-2020.)
⊢ △ = (𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥))))
Syntax	cfwddifn 37103	Declare the syntax for the nth forward difference operator.
class △n
Definition	df-fwddifn 37104*	Define the nth forward difference operator. This works out to be the forward difference operator iterated 𝑛 times. (Contributed by Scott Fenton, 28-May-2020.)
⊢ △n = (𝑛 ∈ ℕ0, 𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · (( -1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))))
Theorem	fwddifval 37105	Calculate the value of the forward difference operator at a point. (Contributed by Scott Fenton, 18-May-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑋 + 1) ∈ 𝐴)    ⇒   ⊢ (𝜑 → (( △ ‘𝐹)‘𝑋) = ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋)))
Theorem	fwddifnval 37106*	The value of the forward difference operator at a point. (Contributed by Scott Fenton, 28-May-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑋 + 𝑘) ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑁 △n 𝐹)‘𝑋) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · (( -1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))
Theorem	fwddifn0 37107	The value of the n-iterated forward difference operator at zero is just the function value. (Contributed by Scott Fenton, 28-May-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((0 △n 𝐹)‘𝑋) = (𝐹‘𝑋))
Theorem	fwddifnp1 37108*	The value of the n-iterated forward difference at a successor. (Contributed by Scott Fenton, 28-May-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑋 + 𝑘) ∈ 𝐴)    ⇒   ⊢ (𝜑 → (((𝑁 + 1) △n 𝐹)‘𝑋) = (((𝑁 △n 𝐹)‘(𝑋 + 1)) − ((𝑁 △n 𝐹)‘𝑋)))
21.12.19  Rank theorems
Theorem	rank0 37109	The rank of the empty set is ∅. (Contributed by Scott Fenton, 17-Jul-2015.)
⊢ (rank‘∅) = ∅
Theorem	rankeq1o 37110	The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.)
⊢ ((rank‘𝐴) = 1o ↔ 𝐴 = {∅})
21.12.20  Hereditarily Finite Sets
Theorem	hftr 37111	The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ Tr HF
Theorem	hfext 37112*	Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ((𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ HF (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)))
Theorem	hfninf 37113	ω is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ¬ ω ∈ HF
21.12.21  Natural ordinal operations
Syntax	cnmul 37114	Declare the syntax for natural multiplication.
class ·no
Definition	df-nmul 37115*	Define natural ordinal multiplication. This is the corresponding operation to df-nadd 8703. (Contributed by Scott Fenton, 2-Jun-2026.)
⊢ ·no = frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), (𝑝 ∈ V, 𝑚 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑎⦌⦋(2nd ‘𝑝) / 𝑏⦌∩ {𝑧 ∈ On ∣ ∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑)) ∈ (𝑧 +no (𝑐𝑚𝑑))}))
Theorem	nmulfn 37116	Natural multiplication is a function over pairs of ordinals. (Contributed by Scott Fenton, 2-Jun-2026.)
⊢ ·no Fn (On × On)
Theorem	nmulprop 37117*	Show closure and value of natural multiplication. (Contributed by Scott Fenton, 2-Jun-2026.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·no 𝐵) ∈ On ∧ (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
Theorem	nmulcl 37118	Closure law for natural multiplication. (Contributed by Scott Fenton, 10-Jun-2026.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·no 𝐵) ∈ On)
Theorem	nmulval 37119*	Show the value of natural multiplication. (Contributed by Scott Fenton, 10-Jun-2026.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
Theorem	nmulcld 37120	Closure law for natural multiplication. Deduction form. (Contributed by Scott Fenton, 12-Jun-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    ⇒   ⊢ (𝜑 → (𝐴 ·no 𝐵) ∈ On)
Theorem	nmulcom 37121	Natural multiplication is commutative. (Contributed by Scott Fenton, 10-Jun-2026.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·no 𝐵) = (𝐵 ·no 𝐴))
Theorem	nmulr0 37122	Natural multiplication by zero. (Contributed by Scott Fenton, 10-Jun-2026.)
⊢ (𝐴 ∈ On → (𝐴 ·no ∅) = ∅)
Theorem	nmull0 37123	Natural multiplication by zero. (Contributed by Scott Fenton, 10-Jun-2026.)
⊢ (𝐴 ∈ On → (∅ ·no 𝐴) = ∅)
Theorem	nmulrid 37124	Identity law for natural multiplication. (Contributed by Scott Fenton, 21-Jul-2026.)
⊢ (𝐴 ∈ On → (𝐴 ·no 1o) = 𝐴)
Theorem	nmullid 37125	Identity law for natural multiplication. (Contributed by Scott Fenton, 21-Jul-2026.)
⊢ (𝐴 ∈ On → (1o ·no 𝐴) = 𝐴)
Theorem	onelond 37126	An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. Lemma 1.3 of [Schloeder] p. 1. Deduction form. (Contributed by Scott Fenton, 31-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ On)
Theorem	ontr2d 37127	Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40. Deduction form. (Contributed by Scott Fenton, 31-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐶)
Theorem	onelssd 37128	An element of an ordinal number is a subset of the number. Deduction form. (Contributed by Scott Fenton, 31-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
Theorem	nmulr0d 37129	Natural multiplication by zero. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    ⇒   ⊢ (𝜑 → (𝐴 ·no ∅) = ∅)
Theorem	nmull0d 37130	Natural multiplication by zero. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    ⇒   ⊢ (𝜑 → (∅ ·no 𝐴) = ∅)
Theorem	nmulridd 37131	Identity law for natural multiplication. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    ⇒   ⊢ (𝜑 → (𝐴 ·no 1o) = 𝐴)
Theorem	nmullidd 37132	Identity law for natural multiplication. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    ⇒   ⊢ (𝜑 → (1o ·no 𝐴) = 𝐴)
Theorem	nmulcomd 37133	Natural multiplication commutes. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    ⇒   ⊢ (𝜑 → (𝐴 ·no 𝐵) = (𝐵 ·no 𝐴))
Theorem	naddridd 37134	Identity law for natural addition. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    ⇒   ⊢ (𝜑 → (𝐴 +no ∅) = 𝐴)
Theorem	naddlidd 37135	Identity law for natural addition. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    ⇒   ⊢ (𝜑 → (∅ +no 𝐴) = 𝐴)
Theorem	naddcomd 37136	Natural addition commutes. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    ⇒   ⊢ (𝜑 → (𝐴 +no 𝐵) = (𝐵 +no 𝐴))
Theorem	naddassd 37137	Natural addition associates. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    ⇒   ⊢ (𝜑 → ((𝐴 +no 𝐵) +no 𝐶) = (𝐴 +no (𝐵 +no 𝐶)))
Theorem	nadd32d 37138	Commutative/associative law that swaps the last two terms in a triple sum. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    ⇒   ⊢ (𝜑 → ((𝐴 +no 𝐵) +no 𝐶) = ((𝐴 +no 𝐶) +no 𝐵))
Theorem	nmuladdel 37139	Ordering relationship for natural ordinal operations. (Contributed by Scott Fenton, 15-Jul-2026.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵)) → ((𝐶 ·no 𝐵) +no (𝐴 ·no 𝐷)) ∈ ((𝐴 ·no 𝐵) +no (𝐶 ·no 𝐷)))
Theorem	nmuladdss 37140	Ordering relationship for natural ordinal operations. (Contributed by Scott Fenton, 15-Jul-2026.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵)) → ((𝐶 ·no 𝐵) +no (𝐴 ·no 𝐷)) ⊆ ((𝐴 ·no 𝐵) +no (𝐶 ·no 𝐷)))
Theorem	nmulss1 37141	Natural multiplication preserves less-than or equal. (Contributed by Scott Fenton, 15-Jul-2026.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (𝐶 ·no 𝐴) ⊆ (𝐶 ·no 𝐵))
Theorem	nmulel1 37142	Natural multiplication by a non-zero number preserves less-than. (Contributed by Scott Fenton, 15-Jul-2026.)
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅)) → (𝐶 ·no 𝐴) ∈ (𝐶 ·no 𝐵))
Theorem	ltnmul 37143*	Characterize less-than a natural product. (Contributed by Scott Fenton, 15-Jul-2026.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ (𝐵 ·no 𝐶) ↔ ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 (𝐴 +no (𝑏 ·no 𝑐)) ⊆ ((𝑏 ·no 𝐶) +no (𝐵 ·no 𝑐))))
Theorem	nmulle 37144*	A condition for bounding a natural product above. Converse of ltnmul 37143. (Contributed by Scott Fenton, 16-Jul-2026.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ·no 𝐵) ⊆ 𝐶 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝐶 +no (𝑎 ·no 𝑏))))
Theorem	ltnadd 37145*	Condition for bounding a natural sum below. (Contributed by Scott Fenton, 21-Jul-2026.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ (𝐵 +no 𝐶) ↔ (∃𝑏 ∈ 𝐵 𝐴 ⊆ (𝑏 +no 𝐶) ∨ ∃𝑐 ∈ 𝐶 𝐴 ⊆ (𝐵 +no 𝑐))))
Theorem	naddle 37146*	Condition for bounding natural addition above. (Contributed by Scott Fenton, 21-Jul-2026.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +no 𝐵) ⊆ 𝐶 ↔ (∀𝑎 ∈ 𝐴 (𝑎 +no 𝐵) ∈ 𝐶 ∧ ∀𝑏 ∈ 𝐵 (𝐴 +no 𝑏) ∈ 𝐶)))
Theorem	nadddilem1 37147*	Lemma for nadddi 37151. Prove a subcase of the reverse implication. (Contributed by Scott Fenton, 31-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 (𝑑 ·no (𝐵 +no 𝐶)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝐶)))    &   ⊢ (𝜑 → ∀𝑓 ∈ 𝐶 (𝐴 ·no (𝐵 +no 𝑓)) = ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝑓)))    &   ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 ∀𝑓 ∈ 𝐶 (𝑑 ·no (𝐵 +no 𝑓)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝑓)))    ⇒   ⊢ ((𝜑 ∧ 𝑌 ∈ (𝐴 ·no 𝐶)) → ((𝐴 ·no 𝐵) +no 𝑌) ∈ (𝐴 ·no (𝐵 +no 𝐶)))
Theorem	nadddilem2 37148*	Lemma for nadddi 37151. Prove the reverse implication. (Contributed by Scott Fenton, 31-Jul-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 (𝑑 ·no (𝐵 +no 𝐶)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝐶)))    &   ⊢ (𝜑 → ∀𝑒 ∈ 𝐵 (𝐴 ·no (𝑒 +no 𝐶)) = ((𝐴 ·no 𝑒) +no (𝐴 ·no 𝐶)))    &   ⊢ (𝜑 → ∀𝑓 ∈ 𝐶 (𝐴 ·no (𝐵 +no 𝑓)) = ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝑓)))    &   ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 ∀𝑒 ∈ 𝐵 (𝑑 ·no (𝑒 +no 𝐶)) = ((𝑑 ·no 𝑒) +no (𝑑 ·no 𝐶)))    &   ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 ∀𝑓 ∈ 𝐶 (𝑑 ·no (𝐵 +no 𝑓)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝑓)))    ⇒   ⊢ (𝜑 → ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝐶)) ⊆ (𝐴 ·no (𝐵 +no 𝐶)))
Theorem	nadddilem3 37149*	Lemma for nadddi 37151. Prove a subcase of the forward implication. (Contributed by Scott Fenton, 3-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 +no 𝐶))    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ⊆ (𝑍 +no 𝐶))    &   ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 (𝑑 ·no (𝐵 +no 𝐶)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝐶)))    &   ⊢ (𝜑 → ∀𝑒 ∈ 𝐵 (𝐴 ·no (𝑒 +no 𝐶)) = ((𝐴 ·no 𝑒) +no (𝐴 ·no 𝐶)))    &   ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 ∀𝑒 ∈ 𝐵 (𝑑 ·no (𝑒 +no 𝐶)) = ((𝑑 ·no 𝑒) +no (𝑑 ·no 𝐶)))    ⇒   ⊢ (𝜑 → ((𝑋 ·no (𝐵 +no 𝐶)) +no (𝐴 ·no 𝑌)) ∈ (((𝐴 ·no 𝐵) +no (𝐴 ·no 𝐶)) +no (𝑋 ·no 𝑌)))
Theorem	nadddilem4 37150*	Lemma for nadddi 37151. Prove the forward implication. (Contributed by Scott Fenton, 3-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 (𝑑 ·no (𝐵 +no 𝐶)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝐶)))    &   ⊢ (𝜑 → ∀𝑒 ∈ 𝐵 (𝐴 ·no (𝑒 +no 𝐶)) = ((𝐴 ·no 𝑒) +no (𝐴 ·no 𝐶)))    &   ⊢ (𝜑 → ∀𝑓 ∈ 𝐶 (𝐴 ·no (𝐵 +no 𝑓)) = ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝑓)))    &   ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 ∀𝑒 ∈ 𝐵 (𝑑 ·no (𝑒 +no 𝐶)) = ((𝑑 ·no 𝑒) +no (𝑑 ·no 𝐶)))    &   ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 ∀𝑓 ∈ 𝐶 (𝑑 ·no (𝐵 +no 𝑓)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝑓)))    ⇒   ⊢ (𝜑 → (𝐴 ·no (𝐵 +no 𝐶)) ⊆ ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝐶)))
Theorem	nadddi 37151	Natural multiplication distributes over natural addition. (Contributed by Scott Fenton, 27-Jul-2026.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ·no (𝐵 +no 𝐶)) = ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝐶)))
Theorem	nadddid 37152	Natural multiplication distributes over natural addition. Deduction form. (Contributed by Scott Fenton, 3-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    ⇒   ⊢ (𝜑 → (𝐴 ·no (𝐵 +no 𝐶)) = ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝐶)))
Theorem	nadddird 37153	Natural multiplication distributes over natural addition. Deduction form. (Contributed by Scott Fenton, 3-Aug-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    ⇒   ⊢ (𝜑 → ((𝐴 +no 𝐵) ·no 𝐶) = ((𝐴 ·no 𝐶) +no (𝐵 ·no 𝐶)))
21.13  Mathbox for Gino Giotto
21.13.1  Equality theorems
21.13.1.1  Inference versions
Theorem	rmoeqi 37154	Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓)
Theorem	rmoeqbii 37155	Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒)
Theorem	reueqi 37156	Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜓)
Theorem	reueqbii 37157	Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒)
Theorem	sbceqbii 37158	Formula-building inference for class substitution. General version of sbcbii 3798. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜓)
Theorem	disjeq1i 37159	Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)
Theorem	disjeq12i 37160	Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷)
Theorem	rabeqbii 37161	Equality theorem for restricted class abstractions. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓}
Theorem	iuneq12i 37162	Equality theorem for indexed union. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷
Theorem	iineq1i 37163	Equality theorem for indexed intersection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶
Theorem	iineq12i 37164	Equality theorem for indexed intersection. Inference version. General version of iineq1i 37163. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷
Theorem	riotaeqbii 37165	Equivalent wff's and equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓)
Theorem	riotaeqi 37166	Equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑)
Theorem	ixpeq1i 37167	Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶
Theorem	ixpeq12i 37168	Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷
Theorem	sumeq2si 37169	Equality inference for sum. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶
Theorem	sumeq12si 37170	Equality inference for sum. General version of sumeq2si 37169. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ Σ𝑥 ∈ 𝐴 𝐶 = Σ𝑥 ∈ 𝐵 𝐷
Theorem	prodeq2si 37171	Equality inference for product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶
Theorem	prodeq12si 37172	Equality inference for product. General version of prodeq2si 37171. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∏𝑥 ∈ 𝐴 𝐶 = ∏𝑥 ∈ 𝐵 𝐷
Theorem	itgeq12i 37173	Equality inference for an integral. General version of itgeq1i 37174 and itgeq2i 37175. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥
Theorem	itgeq1i 37174	Equality inference for an integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥
Theorem	itgeq2i 37175	Equality inference for an integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥
Theorem	ditgeq123i 37176	Equality inference for the directed integral. General version of ditgeq12i 37177 and ditgeq3i 37178. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    &   ⊢ 𝐸 = 𝐹    ⇒   ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥
Theorem	ditgeq12i 37177	Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥
Theorem	ditgeq3i 37178	Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐶 = 𝐷    ⇒   ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥
21.13.1.2  Deduction versions
Theorem	rmoeqdv 37179*	Formula-building rule for restricted at-most-one quantifier. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓))
Theorem	rmoeqbidv 37180*	Formula-building rule for restricted at-most-one quantifier. Deduction form. General version of rmobidv 3384. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒))
Theorem	sbequbidv 37181*	Deduction substituting both sides of a biconditional. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝑢 = 𝑣)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑢 / 𝑥]𝜓 ↔ [𝑣 / 𝑥]𝜒))
Theorem	disjeq12dv 37182*	Equality theorem for disjoint collection. Deduction version. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷))
Theorem	ixpeq12dv 37183*	Equality theorem for infinite Cartesian product. Deduction version. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷)
Theorem	sumeq12sdv 37184*	Equality deduction for sum. General version of sumeq2sdv 15899. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷)
Theorem	prodeq12sdv 37185*	Equality deduction for product. General version of prodeq2sdv 16120. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷)
Theorem	itgeq12sdv 37186*	Equality theorem for an integral. Deduction form. General version of itgeq1d 47172 and itgeq2sdv 37187. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥)
Theorem	itgeq2sdv 37187*	Equality theorem for an integral. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥)
Theorem	ditgeq123dv 37188*	Equality theorem for the directed integral. Deduction form. General version of ditgeq3sdv 37190. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥)
Theorem	ditgeq12d 37189*	Equality theorem for the directed integral. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥)
Theorem	ditgeq3sdv 37190*	Equality theorem for the directed integral. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥)
21.13.2  Change bound variables
Theorem	in-ax8 37191	A proof of ax-8 2149 that does not rely on ax-8 2149. It employs df-in 4094 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2157. Since the nature of this result is unclear, usage of this theorem is discouraged, and this method should not be applied to eliminate axiom dependencies. (Contributed by GG, 1-Aug-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
Theorem	ss-ax8 37192	A proof of ax-8 2149 that does not rely on ax-8 2149. It employs df-ss 3901 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2157. Contrary to in-ax8 37191, this proof does not rely on df-cleq 2755, therefore using fewer axioms . This method should not be applied to eliminate axiom dependencies. (Contributed by GG, 30-Aug-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
21.13.2.1  Change bound variables and domains
Theorem	cbvralvw2 37193*	Change bound variable and domain in the restricted universal quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrexvw2 37194*	Change bound variable and domain in the restricted existential quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrmovw2 37195*	Change bound variable and domain in the restricted at-most-one quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐵 𝜓)
Theorem	cbvreuvw2 37196*	Change bound variable and domain in the restricted existential uniqueness quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓)
Theorem	cbvsbcvw2 37197*	Change bound variable of a class substitution using implicit substitution. General version of cbvsbcvw 3776. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑦]𝜓)
Theorem	cbvcsbvw2 37198*	Change bound variable of a proper substitution into a class using implicit substitution. General version of cbvcsbv 3863. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷
Theorem	cbviunvw2 37199*	Change bound variable and domain in indexed unions, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐵 𝐷
Theorem	cbviinvw2 37200*	Change bound variable and domain in an indexed intersection, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑦 ∈ 𝐵 𝐷