P. 364 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36301-36400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cbvsumvw2 36301*	Change bound variable and the set of integers in a sum, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷)    ⇒   ⊢ Σ𝑗 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷
Theorem	cbvprodvw2 36302*	Change bound variable and the set of integers in a product, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷)    ⇒   ⊢ ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷
Theorem	cbvitgvw2 36303*	Change bound variable and domain in an integral, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑦
Theorem	cbvditgvw2 36304*	Change bound variable and domain in a directed integral, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    &   ⊢ (𝑥 = 𝑦 → 𝐸 = 𝐹)    ⇒   ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑦
21.12.2.2  Change bound variables, deduction versions.
Theorem	cbvmodavw 36305*	Change bound variable in the at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑦𝜒))
Theorem	cbveudavw 36306*	Change bound variable in the existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑦𝜒))
Theorem	cbvrmodavw 36307*	Change bound variable in the restricted at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑦 ∈ 𝐴 𝜒))
Theorem	cbvreudavw 36308*	Change bound variable in the restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐴 𝜒))
Theorem	cbvsbdavw 36309*	Change bound variable in proper substitution. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑦]𝜒))
Theorem	cbvsbdavw2 36310*	Change bound variable in proper substitution. General version of cbvsbdavw 36309. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝑧 = 𝑤)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑤 / 𝑦]𝜒))
Theorem	cbvabdavw 36311*	Change bound variable in class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑦 ∣ 𝜒})
Theorem	cbvsbcdavw 36312*	Change bound variable of a class substitution. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑦]𝜒))
Theorem	cbvsbcdavw2 36313*	Change bound variable of a class substitution. General version of cbvsbcdavw 36312. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑦]𝜒))
Theorem	cbvcsbdavw 36314*	Change bound variable of a proper substitution into a class. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑦⦌𝐶)
Theorem	cbvcsbdavw2 36315*	Change bound variable of a proper substitution into a class. General version of cbvcsbdavw 36314. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷)
Theorem	cbvrabdavw 36316*	Change bound variable in restricted class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∈ 𝐴 ∣ 𝜒})
Theorem	cbviundavw 36317*	Change bound variable in indexed unions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶)
Theorem	cbviindavw 36318*	Change bound variable in indexed intersections. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶)
Theorem	cbvopab1davw 36319*	Change the first bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑧, 𝑦⟩ ∣ 𝜒})
Theorem	cbvopab2davw 36320*	Change the second bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑧⟩ ∣ 𝜒})
Theorem	cbvopabdavw 36321*	Change bound variables in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑧, 𝑤⟩ ∣ 𝜒})
Theorem	cbvmptdavw 36322*	Change bound variable in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶))
Theorem	cbvdisjdavw 36323*	Change bound variable in a disjoint collection. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶))
Theorem	cbviotadavw 36324*	Change bound variable in a description binder. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑦𝜒))
Theorem	cbvriotadavw 36325*	Change bound variable in a restricted description binder. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑦 ∈ 𝐴 𝜒))
Theorem	cbvoprab1davw 36326*	Change the first bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Theorem	cbvoprab2davw 36327*	Change the second bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑧⟩ ∣ 𝜒})
Theorem	cbvoprab3davw 36328*	Change the third bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑧 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜒})
Theorem	cbvoprab123davw 36329*	Change all bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑦 = 𝑢) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑢⟩, 𝑣⟩ ∣ 𝜒})
Theorem	cbvoprab12davw 36330*	Change the first and second bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑦 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑣⟩, 𝑧⟩ ∣ 𝜒})
Theorem	cbvoprab23davw 36331*	Change the second and third bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑦 = 𝑤) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑣⟩ ∣ 𝜒})
Theorem	cbvoprab13davw 36332*	Change the first and third bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑣⟩ ∣ 𝜒})
Theorem	cbvixpdavw 36333*	Change bound variable in an indexed Cartesian product. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶)
Theorem	cbvsumdavw 36334*	Change bound variable in a sum. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑘 = 𝑗) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑗 ∈ 𝐴 𝐶)
Theorem	cbvproddavw 36335*	Change bound variable in a product. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)
Theorem	cbvitgdavw 36336*	Change bound variable in an integral. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑦)
Theorem	cbvditgdavw 36337*	Change bound variable in a directed integral. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦)
21.12.2.3  Change bound variables and domains, deduction versions.
Theorem	cbvrmodavw2 36338*	Change bound variable and quantifier domain in the restricted at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑦 ∈ 𝐵 𝜒))
Theorem	cbvreudavw2 36339*	Change bound variable and quantifier domain in the restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐵 𝜒))
Theorem	cbvrabdavw2 36340*	Change bound variable and domain in restricted class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∈ 𝐵 ∣ 𝜒})
Theorem	cbviundavw2 36341*	Change bound variable and domain in indexed unions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐵 𝐷)
Theorem	cbviindavw2 36342*	Change bound variable and domain in indexed intersections. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑦 ∈ 𝐵 𝐷)
Theorem	cbvmptdavw2 36343*	Change bound variable and domain in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐷))
Theorem	cbvdisjdavw2 36344*	Change bound variable and domain in a disjoint collection. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑦 ∈ 𝐵 𝐷))
Theorem	cbvriotadavw2 36345*	Change bound variable and domain in a restricted description binder. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑦 ∈ 𝐵 𝜒))
Theorem	cbvmpodavw2 36346*	Change bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐸 = 𝐹)    &   ⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)    &   ⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑤 ∈ 𝐷 ↦ 𝐹))
Theorem	cbvmpo1davw2 36347*	Change first bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐸 = 𝐹)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹))
Theorem	cbvmpo2davw2 36348*	Change second bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐸 = 𝐹)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑧 ∈ 𝐷 ↦ 𝐹))
Theorem	cbvixpdavw2 36349*	Change bound variable and domain in an indexed Cartesian product. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑦 ∈ 𝐵 𝐷)
Theorem	cbvsumdavw2 36350*	Change bound variable and the set of integers in a sum. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷)
Theorem	cbvproddavw2 36351*	Change bound variable and the set of integers in a product. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷)
Theorem	cbvitgdavw2 36352*	Change bound variable and domain in an integral. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑦)
Theorem	cbvditgdavw2 36353*	Change bound variable and limits in a directed integral. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑦)
21.12.3  Study of ax-mulf usage.
Theorem	mpomulnzcnf 36354*	Multiplication maps nonzero complex numbers to nonzero complex numbers. Version of mulnzcnf 11773 using maps-to notation, which does not require ax-mulf 11096. (Contributed by GG, 18-Apr-2025.)
⊢ (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑥 · 𝑦)):((ℂ ∖ {0}) × (ℂ ∖ {0}))⟶(ℂ ∖ {0})
21.13  Mathbox for Jeff Hankins
21.13.1  Miscellany
Theorem	a1i14 36355	Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.)
⊢ (𝜓 → (𝜒 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	a1i24 36356	Add two antecedents to a wff. Deduction associated with a1i13 27. (Contributed by Jeff Hankins, 5-Aug-2009.)
⊢ (𝜑 → (𝜒 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp5d 36357	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp5g 36358	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ ((𝜑 ∧ 𝜓) → (((𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp5k 36359	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (((𝜓 ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp56 36360	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp58 36361	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (((𝜑 ∧ 𝜓) ∧ ((𝜒 ∧ 𝜃) ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp510 36362	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ ((𝜑 ∧ (((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp511 36363	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ ((𝜑 ∧ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp512 36364	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏))) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	3com12d 36365	Commutation in consequent. Swap 1st and 2nd. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	imp5p 36366	A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂)))
Theorem	imp5q 36367	A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂))
Theorem	ecase13d 36368	Deduction for elimination by cases. (Contributed by Jeff Hankins, 18-Aug-2009.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	subtr 36369	Transitivity of implicit substitution. (Contributed by Jeff Hankins, 13-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑌    &   ⊢ Ⅎ𝑥𝑍    &   ⊢ (𝑥 = 𝐴 → 𝑋 = 𝑌)    &   ⊢ (𝑥 = 𝐵 → 𝑋 = 𝑍)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 = 𝐵 → 𝑌 = 𝑍))
Theorem	subtr2 36370	Transitivity of implicit substitution into a wff. (Contributed by Jeff Hankins, 19-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 = 𝐵 → (𝜓 ↔ 𝜒)))
Theorem	trer 36371*	A relation intersected with its converse is an equivalence relation if the relation is transitive. (Contributed by Jeff Hankins, 6-Oct-2009.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ))
Theorem	elicc3 36372	An equivalent membership condition for closed intervals. (Contributed by Jeff Hankins, 14-Jul-2009.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ (𝐶 = 𝐴 ∨ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ∨ 𝐶 = 𝐵))))
Theorem	finminlem 36373*	A useful lemma about finite sets. If a property holds for a finite set, it holds for a minimal set. (Contributed by Jeff Hankins, 4-Dec-2009.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ Fin 𝜑 → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))
Theorem	gtinf 36374*	Any number greater than an infimum is greater than some element of the set. (Contributed by Jeff Hankins, 29-Sep-2013.) (Revised by AV, 10-Oct-2021.)
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ (𝐴 ∈ ℝ ∧ inf(𝑆, ℝ, < ) < 𝐴)) → ∃𝑧 ∈ 𝑆 𝑧 < 𝐴)
Theorem	opnrebl 36375*	A set is open in the standard topology of the reals precisely when every point can be enclosed in an open ball. (Contributed by Jeff Hankins, 23-Sep-2013.) (Proof shortened by Mario Carneiro, 30-Jan-2014.)
⊢ (𝐴 ∈ (topGen‘ran (,)) ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ℝ+ ((𝑥 − 𝑦)(,)(𝑥 + 𝑦)) ⊆ 𝐴))
Theorem	opnrebl2 36376*	A set is open in the standard topology of the reals precisely when every point can be enclosed in an arbitrarily small ball. (Contributed by Jeff Hankins, 22-Sep-2013.) (Proof shortened by Mario Carneiro, 30-Jan-2014.)
⊢ (𝐴 ∈ (topGen‘ran (,)) ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ (𝑧 ≤ 𝑦 ∧ ((𝑥 − 𝑧)(,)(𝑥 + 𝑧)) ⊆ 𝐴)))
Theorem	nn0prpwlem 36377*	Lemma for nn0prpw 36378. Use strong induction to show that every positive integer has unique prime power divisors. (Contributed by Jeff Hankins, 28-Sep-2013.)
⊢ (𝐴 ∈ ℕ → ∀𝑘 ∈ ℕ (𝑘 < 𝐴 → ∃𝑝 ∈ ℙ ∃𝑛 ∈ ℕ ¬ ((𝑝↑𝑛) ∥ 𝑘 ↔ (𝑝↑𝑛) ∥ 𝐴)))
Theorem	nn0prpw 36378*	Two nonnegative integers are the same if and only if they are divisible by the same prime powers. (Contributed by Jeff Hankins, 29-Sep-2013.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ ∀𝑛 ∈ ℕ ((𝑝↑𝑛) ∥ 𝐴 ↔ (𝑝↑𝑛) ∥ 𝐵)))
21.13.2  Basic topological facts
Theorem	topbnd 36379	Two equivalent expressions for the boundary of a topology. (Contributed by Jeff Hankins, 23-Sep-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((cls‘𝐽)‘𝐴) ∩ ((cls‘𝐽)‘(𝑋 ∖ 𝐴))) = (((cls‘𝐽)‘𝐴) ∖ ((int‘𝐽)‘𝐴)))
Theorem	opnbnd 36380	A set is open iff it is disjoint from its boundary. (Contributed by Jeff Hankins, 23-Sep-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ 𝐽 ↔ (𝐴 ∩ (((cls‘𝐽)‘𝐴) ∩ ((cls‘𝐽)‘(𝑋 ∖ 𝐴)))) = ∅))
Theorem	cldbnd 36381	A set is closed iff it contains its boundary. (Contributed by Jeff Hankins, 1-Oct-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘𝐽) ↔ (((cls‘𝐽)‘𝐴) ∩ ((cls‘𝐽)‘(𝑋 ∖ 𝐴))) ⊆ 𝐴))
Theorem	ntruni 36382*	A union of interiors is a subset of the interior of the union. The reverse inclusion may not hold. (Contributed by Jeff Hankins, 31-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑂 ⊆ 𝒫 𝑋) → ∪ 𝑜 ∈ 𝑂 ((int‘𝐽)‘𝑜) ⊆ ((int‘𝐽)‘∪ 𝑂))
Theorem	clsun 36383	A pairwise union of closures is the closure of the union. (Contributed by Jeff Hankins, 31-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) → ((cls‘𝐽)‘(𝐴 ∪ 𝐵)) = (((cls‘𝐽)‘𝐴) ∪ ((cls‘𝐽)‘𝐵)))
Theorem	clsint2 36384*	The closure of an intersection is a subset of the intersection of the closures. (Contributed by Jeff Hankins, 31-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐶 ⊆ 𝒫 𝑋) → ((cls‘𝐽)‘∩ 𝐶) ⊆ ∩ 𝑐 ∈ 𝐶 ((cls‘𝐽)‘𝑐))
Theorem	opnregcld 36385*	A set is regularly closed iff it is the closure of some open set. (Contributed by Jeff Hankins, 27-Sep-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((cls‘𝐽)‘((int‘𝐽)‘𝐴)) = 𝐴 ↔ ∃𝑜 ∈ 𝐽 𝐴 = ((cls‘𝐽)‘𝑜)))
Theorem	cldregopn 36386*	A set if regularly open iff it is the interior of some closed set. (Contributed by Jeff Hankins, 27-Sep-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (((int‘𝐽)‘((cls‘𝐽)‘𝐴)) = 𝐴 ↔ ∃𝑐 ∈ (Clsd‘𝐽)𝐴 = ((int‘𝐽)‘𝑐)))
Theorem	neiin 36387	Two neighborhoods intersect to form a neighborhood of the intersection. (Contributed by Jeff Hankins, 31-Aug-2009.)
⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝑀 ∩ 𝑁) ∈ ((nei‘𝐽)‘(𝐴 ∩ 𝐵)))
Theorem	hmeoclda 36388	Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.) (Revised by Mario Carneiro, 3-Jun-2014.)
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ (𝐽Homeo𝐾)) ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑆) ∈ (Clsd‘𝐾))
Theorem	hmeocldb 36389	Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009.)
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ (𝐽Homeo𝐾)) ∧ 𝑆 ∈ (Clsd‘𝐾)) → (◡𝐹 “ 𝑆) ∈ (Clsd‘𝐽))
21.13.3  Topology of the real numbers
Theorem	ivthALT 36390*	An alternate proof of the Intermediate Value Theorem ivth 25392 using topology. (Contributed by Jeff Hankins, 17-Aug-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑈 ∈ ℝ) ∧ 𝐴 < 𝐵 ∧ ((𝐴[,]𝐵) ⊆ 𝐷 ∧ 𝐷 ⊆ ℂ ∧ (𝐹 ∈ (𝐷–cn→ℂ) ∧ (𝐹 “ (𝐴[,]𝐵)) ⊆ ℝ ∧ 𝑈 ∈ ((𝐹‘𝐴)(,)(𝐹‘𝐵))))) → ∃𝑥 ∈ (𝐴(,)𝐵)(𝐹‘𝑥) = 𝑈)
21.13.4  Refinements
Syntax	cfne 36391	Extend class definition to include the "finer than" relation.
class Fne
Definition	df-fne 36392*	Define the fineness relation for covers. (Contributed by Jeff Hankins, 28-Sep-2009.)
⊢ Fne = {⟨𝑥, 𝑦⟩ ∣ (∪ 𝑥 = ∪ 𝑦 ∧ ∀𝑧 ∈ 𝑥 𝑧 ⊆ ∪ (𝑦 ∩ 𝒫 𝑧))}
Theorem	fnerel 36393	Fineness is a relation. (Contributed by Jeff Hankins, 28-Sep-2009.)
⊢ Rel Fne
Theorem	isfne 36394*	The predicate "𝐵 is finer than 𝐴". This property is, in a sense, the opposite of refinement, as refinement requires every element to be a subset of an element of the original and fineness requires that every element of the original have a subset in the finer cover containing every point. I do not know of a literature reference for this. (Contributed by Jeff Hankins, 28-Sep-2009.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐵 ∈ 𝐶 → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥))))
Theorem	isfne4 36395	The predicate "𝐵 is finer than 𝐴 " in terms of the topology generation function. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ 𝐴 ⊆ (topGen‘𝐵)))
Theorem	isfne4b 36396	A condition for a topology to be finer than another. (Contributed by Jeff Hankins, 28-Sep-2009.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐵 ∈ 𝑉 → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ (topGen‘𝐴) ⊆ (topGen‘𝐵))))
Theorem	isfne2 36397*	The predicate "𝐵 is finer than 𝐴". (Contributed by Jeff Hankins, 28-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐵 ∈ 𝐶 → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))))
Theorem	isfne3 36398*	The predicate "𝐵 is finer than 𝐴". (Contributed by Jeff Hankins, 11-Oct-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐵 ∈ 𝐶 → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))))
Theorem	fnebas 36399	A finer cover covers the same set as the original. (Contributed by Jeff Hankins, 28-Sep-2009.)
⊢ 𝑋 = ∪ 𝐴    &   ⊢ 𝑌 = ∪ 𝐵    ⇒   ⊢ (𝐴Fne𝐵 → 𝑋 = 𝑌)
Theorem	fnetg 36400	A finer cover generates a topology finer than the original set. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (𝐴Fne𝐵 → 𝐴 ⊆ (topGen‘𝐵))